[isabelle-dev] NEWS: Improved completion based on context information

[Makarius]

On Fri, 21 Feb 2014, Makarius wrote:

> * Improved completion based

The next round of tuning and improvements is Isabelle/96ddf9bf12ac. Some 
general notes how this works:

   * In certain situations the prover produces semantic completion of a
     list of names (from the formal name space).  If this is available it
     takes precedence over anything else, but it requires a full round-trip
     through PIDE document processing to become available.  (I am still
     working on the fact name space problem.)

   * Otherwise, there is a language context provided by the outer parsers
     or other syntax layers.  This information is used for syntactic
     completion: keywords, symbols, antiquotations, depending on the
     language specification (see also ~~/src/Pure/PIDE/markup.ML
     language_XYZ).  Lack of language context markup means "outer syntax"
     as before.  ML files have their own outer language context, in
     contrast to inner syntax of ML comments and strings.

   * A blue frame is painted over an active completion range (popup
     visible), or a possible completion.  In the latter case, explicit
     completion via C+b (jEdit action via menu etc.) takes the available
     information to insert into the buffer, or produce a popup.

I've made two or three rounds of testing with the rather aggressive 
options:

    completion_delay = 0.0
    completion_immediate = true

The "feel" of it is quite good so far, but their might be snags and 
confusing effects remaining.  This is an interactive computer game, after 
all.

Unexpected completion (or lack thereof) might be a cause of the language 
context (or lack thereof).  The C-hover-mouse idiom reveals tooltip 
information of "language: NAME" and a grey region behind it.


Any further observations by other early adopters of this important 
mechanism?


 	Makarius