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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
