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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
