[isabelle-dev] NEWS: Improved completion mechanism

[Christian Sternagel]

Dear Makarius,

First note that for me keyboard input to Isabelle/jEdit typically hangs 
every 10 minutes or so, depending on how fast I type (but this is an old 
and known issue).

In Isabelle2013 the completion popup was not triggered when deleting 
characters (with backspace). Now this is the case and it seems to cause 
more frequent hangs for me (since deleting is typically done very fast). 
Is this behavior intentional, and if yes, what is the gain?

cheers

chris

On 08/30/2013 08:52 PM, Makarius wrote:
> * 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
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev