[isabelle-dev] NEWS: improved syntactic and semantic completion mechanism
makarius at sketis.net
Wed May 21 22:20:29 CEST 2014
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 :-)
More information about the isabelle-dev