[isabelle-dev] Immediate completion does not work anymore

[Manuel Eberl]

Lars just informed me that I didn't actually include an example in my 
mail (I thought I did); it was therefore probably not clear what I meant 
exactly, so let me explain:

When I write "\ci" in a theory, it used to be completed to ∘ 
immediately. As of 1ca11ddfcc70, this does not happen anymore; I have to 
complete it manually. The same happens with every other backslash 
abbreviation I tried. Is this the intended behaviour? If it is, I'm 
afraid I find that somewhat unpleasant.


As an unrelated issue: convergence of functions/sequences is written as 
"op --->" / "op ---->". Entering this arrow is somewhat painful when 
immediate completion is turned on, since it completes to "-⟶" / "--⟶". 
Is there anything that can be done about that?


Cheers,

Manuel