[isabelle-dev] NEWS: improved syntactic and semantic completion mechanism

[Makarius]

*** Prover IDE -- Isabelle/Scala/jEdit ***

* Improved syntactic and semantic completion mechanism:

   - No completion for Isar keywords that have already been recognized
     by the prover, e.g. ":" within accepted Isar syntax looses its
     meaning as abbreviation for symbol "\<in>".

   - Completion context provides information about embedded languages
     of Isabelle: keywords are only completed for outer syntax, symbols
     or antiquotations for languages that support them.  E.g. no symbol
     completion for ML source, but within ML strings, comments,
     antiquotations.

   - Support for semantic completion based on failed name space lookup.
     The error produced by the prover contains information about
     alternative names that are accessible in a particular position.
     This may be used with explicit completion (C+b) or implicit
     completion after some delay.

   - Semantic completions may get extended by appending a suffix of
     underscores to an already recognized name, e.g. "foo_" to complete
     "foo" or "foobar" if these are known in the context.  The special
     identifier "__" serves as a wild-card in this respect: it
     completes to the full collection of names from the name space
     (truncated according to the system option "completion_limit").

   - Syntax completion of the editor and semantic completion of the
     prover are merged.  Since the latter requires a full round-trip of
     document update to arrive, the default for option
     jedit_completion_delay has been changed to 0.5s to improve the
     user experience.

   - Option jedit_completion_immediate may now get used with
     jedit_completion_delay > 0, to complete symbol abbreviations
     aggressively while benefiting from combined syntactic and semantic
     completion.

   - Support for simple completion templates (with single
     place-holder), e.g. "`" for text cartouche, or "@{" for
     antiquotation.

   - Improved treatment of completion vs. various forms of jEdit text
     selection (multiple selections, rectangular selections,
     rectangular selection as "tall caret").

   - More reliable treatment of GUI events vs. completion popups: avoid
     loosing keystrokes with slow / remote graphics displays.


These cumulative NEWS refer to Isabelle/075397022503.  This also marks the 
point where my continously shrinking and growing TODO list has reached a 
stable state concerning "completion" and the main activity on this part is 
finished for now.

The coming weeks and months are the opportunity to figure out minor snags 
and missing bits of completion, *before* we embark on the release in 
summer.  Although it is a slow and painful process for me to make these 
things work, my impression is that the "consumption" of such novelties are 
even slower and more painful, and very little actual testing happens. 
Completion is particularly critical, because it sits right in the main key 
event loop of the editor.

Note that the above changes of default options are not pushed onto people 
who are hooked on the repository, because the options from 
$ISABELLE_HOME_USER take precedence.  It is also worth trying variations 
like this:

   jedit_completion = true
   jedit_completion_delay = 0.5
   jedit_completion_immediate = true

Thus former ASCII replacement syntax like ==> --> <= etc. become readily 
available as quick input method.  Moreover it is always possible to use 
single letter abbreviations like : ! & | with explicit C+b (without silly 
replacements for Isar keywords that the prover has already recognized). 
Ultimately, the improved support for multi-selections helps to use 
hypersearch on ASCII replacement syntax with C+b replacement -- next time 
we do that semantically, as "refactoring" :-)


 	Makarius