[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

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 

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.


More information about the isabelle-dev mailing list