[isabelle-dev] NEWS: improved syntactic and semantic completion mechanism

[Makarius]

On Wed, 21 May 2014, Lars Noschinski wrote:

> I switched back to 0s. Enabling immediate completion did not make this 
> more palatable for me, for two reasons: For example, "!" is not 
> immediately completed (due to "!!").

Note that single-character abbreviations are never completed.  I started 
with that in the very beginning, but found it so confusion that I stopped 
it immediately.  You can in principle define your own abbreviations of 
more than one character to get immediate \<forall> nonetheless.


> I usually feel that I mistyped and hit backspace immediately - if the 
> word was completed in between, I should have hit Ctrl-Z instead.

The now extinct X-symbol mode of Emacs had the same principle to use 
regular undo to undo an unwanted completion.  Unlike Emacs, jEdit selects 
the undone region afterwards, which is the explicit intention of the jEdit 
guys, so an extra ESCAPE is needed in practice.  (Or one could allocate 
shift-capslock to undo a completion :-)


 	Makarius