[isabelle-dev] NEWS: Improved completion mechanism
makarius at sketis.net
Wed Sep 4 14:00:34 CEST 2013
On Fri, 30 Aug 2013, Makarius wrote:
> * Improved completion mechanism, which is now managed by the
> Isabelle/jEdit plugin instead of SideKick.
> - Refined table of Isabelle symbol abbreviations (see
This came out a bit terse as an explanation.
There is an arbitrary relation between symbols and abbrevs (without
requiring uniqueness); it is specified via $ISABELLE_HOME/etc/symbols and
$ISABELLE_HOME_USER/etc/symbols (provided by ambitious users).
The completion mechanism tries to be smart in doing just the right thing
at the right time (after 2-3 rounds of refinement, a few more might be
The subsequent examples are for the somewhat aggressive "expert mode":
jedit_completion = true
jedit_completion_delay = 0.0
jedit_completion_immediate = true
A single "!" in the text will produce a popup, even if there there is just
a single choice. A more explicit completion candidate like "!!" or "==>"
is immediately inserted with its unique completion; if that was unintended
plain undo will revert it just like ancient X-Symbol in PG 3.x.
Non-unique completions like <> or <-> always make a popup with a choice of
arrows, but <--> is again unique so it immediately inserts a long double
The order of the list in popups adapts dynamically according to the
frequency of use of certain replacements. This information does not
affect the general completion policies, though.
Some symbol abbrevs never have an effect in implicit completion, since
they are too short. They work with explicit C+b and help to upgrade
really ancient theory sources that still use ALL, EX, UN, INT, Un, Int
Backslashed text like "\a" is considered explicit enough to be implicitly
completable. The frequency counter will rather quickly put e.g. greek
letters first according to their use. It requires some practice to know
how much explicit text is required to get greeks etc. immediately without
popup, but that behaviour won't change according to frequency of use.
I recommend to go through the $ISABELLE_HOME/etc/symbols with its 'abbrev'
specifications and practice a little bit (and point out totally strange
and unexpected behaviour.)
More information about the isabelle-dev