[isabelle-dev] NEWS: Improved completion mechanism

[Makarius]

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
>    $ISABELLE_HOME/etc/symbols).

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 
coming).


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 
arrow.

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 
etc.

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.)


 	Makarius