[isabelle-dev] Facts and semantic completion

[Makarius]

Attentive readers of incoming change history may have already noticed more 
and more support for semantic completion.  The present situation in 
Isabelle/c06202417c4a is as follows, especially about the inclusion of the 
facts name space.


First some general principles:

  * Semantic completion works via failed name space lookups: the error
    message contains information about alternative names that would
    succeed.  The Prover IDE includes that information in the key event
    handler that is responsible for the completion popup, or in explicit
    completion via C+b.

  * Semantic completion takes precedence over syntactic one, but I will
    probably change that and merge the two sources of information.

  * Completion of something that is formally already recognized is usually
    avoided.  E.g. the ":" that is known as Isar keyword no longer works as
    symbol abbreviation for "\<in>", but the system needs a full PIDE
    protocol round trip to discover that.

  * A suffix of one or more underscores can be used to "extend" already
    recognized input, by forcing a failure and causing an alternative name
    selection (trailing underscores hardly ever occur in legal names).
    The special name "__" serves as wild card: in completes to everything
    (truncated by the usual completion_limit).

  * Corollary: within the term language, unrecognized consts are accepted
    as frees, so they are *not* completed by default.  After adding an
    underscore or using "__" outright, resolution via the consts name space
    is enforced and leads to completion of the same.

  * Classes, types, and almost everything else complete more easily since
    there is only one name space to take into account.  Any prefix of a
    name that is not yet accepted works, but underscores sometimes help
    extending the completion, and "__" always works.


Facts did not participate in this game so far, due to the slightly odd 
arrangement of a stricly local facts space that was backed-up by a global 
one, with two unrelated attempts of name space lookup.  I've tried several 
ways to unify this into just one name space, i.e. a local one initialized 
from the background theory that accumulates all updates from the theory or 
context according to the local_theory discipline of types and consts 
(which was the subject of performance improvements in 4d46d53566e6).

Unfortunetely, all this smart change table management did not suffice to 
make full merges of facts sufficiently fast.  In many situations more time 
was spent managing facts than doing proofs. Today in ed92ce2ac88e, I've 
also tried a more conventional approach of local theory targets to 
distribute background theory updates to all participating contexts of the 
local theory sandwich, by replaying the update functions directly instead 
of merging the data, but it was still causing a slowdown within the range 
of factor 1.2 .. 2.0 for various sessions.


The presently active approach c06202417c4a is a variant of that: there are 
again two fact spaces, but the local one is initialized from the 
background theory *without* participating in its updates.  Thus a locale 
or class target may lack access to certain background facts outside of its 
axiomatic context that are produced *after* the target initialization. 
To amend that deficiency, the fact lookup uses the global table as 
fall-back as was done in the past, but the completion error message is 
always that of the local table.

This approach is a tiny bit less complicated than the old one with two 
tables concatenated in a messy way.  It also performs somewhat better than 
the single cumulative facts space.  Moreover it gives almost accurate 
completion results in most practical situations: all of Isabelle + AFP 
requires only about 100 background facts that are not in the local space 
--- the user needs to know that they are there, because completion will 
not show them.  Thousands of other facts are properly acessible, though.


So the conclusion of the story so far: I need to keep an eye on the full 
performance implications of c06202417c4a.  Moreover, early adopters are 
invited to explore the possibilites to edit theory sources mainly with two 
keys: "_" and TAB.  (The machanics of the GUI popup are still that of last 
summer, but that is a different story.)


 	Makarius