[isabelle-dev] NEWS: Improved completion mechanism
Makarius
makarius at sketis.net
Fri Aug 30 13:52:57 CEST 2013
* Improved completion mechanism, which is now managed by the
Isabelle/jEdit plugin instead of SideKick.
- Various Isabelle plugin options to control popup behaviour and
immediate insertion into buffer.
- Light-weight popup, which avoids explicit window (more reactive
and more robust). Interpreted key events: TAB, ESCAPE, UP, DOWN,
PAGE_UP, PAGE_DOWN. All other key events are passed to the jEdit
text area unchanged.
- Explicit completion via standard jEdit shortcut C+b, which has
been remapped to action "isabelle.complete" (fall-back on regular
"complete-word" for non-Isabelle buffers).
- Implicit completion via keyboard input on text area, with popup or
immediate insertion into buffer.
- Implicit completion of plain words requires at least 3 characters
(was 2 before).
- Immediate completion ignores plain words; it requires > 1
characters of symbol abbreviation to complete, otherwise fall-back
on completion popup.
- Isabelle Symbols are only completed in backslashed forms,
e.g. \forall or \<forall> that both produce the Isabelle symbol
\<forall> in its Unicode rendering.
- Refined table of Isabelle symbol abbreviations (see
$ISABELLE_HOME/etc/symbols).
This refers to Isabelle/d0e4c8f73541. It is an intermediate somewhat
stable stepping-stone -- it remains to be seen which of the other ideas on
my list can be worked out before the release (it is getting quite close
now).
If there are any oddities in the new setup, or really bad things of the
old one that are still there, please let me know about it.
Makarius
More information about the isabelle-dev
mailing list