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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
