[isabelle-dev] Immediate completion does not work anymore
eberlm at in.tum.de
Mon Nov 23 13:56:31 CET 2015
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?
More information about the isabelle-dev