[isabelle-dev] NEWS: Improved completion based on context information
makarius at sketis.net
Wed Feb 26 17:50:56 CET 2014
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
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
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
More information about the isabelle-dev