[isabelle-dev] NEWS: improved syntactic and semantic completion mechanism
makarius at sketis.net
Wed Apr 16 15:57:57 CEST 2014
On Tue, 15 Apr 2014, Lars Noschinski wrote:
> Where C+b is bound to "Complete Isabelle text", I assume (following the
> repository versions, it was still "Complete Word" for me).
Yes. Keyboard defaults cannot be pushed on people hanging on the
repository: jEdit turns the centrally given properties once and for all
into some "imported" keymap, which then remains under control of the user.
Any mentioning of keyboard shortcuts in NEWS or manuals refers to a proper
release, where the initial settings are fresh.
>> - 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"
> I would expect an _explicit_ completion after "foo" to offer both "foo"
> and "foobar". After all, I am apparently not satisfied with the current
There are many side-conditions on the general mechanics. GUI events (like
keystrokes) can only use information that is available on the spot, in the
persistent document content on the Scala side. Producing completion
information is a relatively expensive operation, both time (prover) and
space (editor). Annotating all formal entities -- i.e. the greater part
of the text -- just for the case that the user might request explicit
completion would be quite expensive.
There is also the side-problem of the free vs. consts within the term
language. A non-existing const is accepted as free.
The explicit suffixing with "_" makes the intention clear to the prover,
without much complication or time/space overhead. It should be also
reasonably easy to instruct users to use it.
> I also noticed that "__" is marked as completable, but you need to
> request explicit completion -- is this intended?
I don't think there is anything special here. If you have
jedit_completion_delay = 0.0 then there is nothing to complete on the spot
so you have to request it explicitly later. The continuos update of
information in the background is merely turned into the relatively
non-intrusive blue box, not into a sudden change of the popup status (from
absent to present, or from present with one state to another state).
Nonetheless there might be remaining snags. It requires a lot of
experimentation to converge to a state that somehow works out concerning
technical side-conditions and smoothness in user-experience.
>> - 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.
> With immediate completion, this seems somewhat usable for me (but I
> still need test it more -- for most of my current work I am bound to the
> release version). Without immediate completion, I always have to insert
> artificial pauses for symbol completion, which is very annoying.
There is no need to pause for symbol completions. You merely keep the new
default jedit_completion_delay = 0.5 and say jedit_completion_immediate =
true, such that just the symbol abbreviations are completed on the spot.
This works due to a recent modification:
date: Sun Mar 30 21:03:40 2014 +0200
immediate completion even with delay, which is the default according to
Nonetheless, there were situations where the all-important "language
context" could not be retrieved, when editing too quickly. I have refined
that just yesterday here:
date: Tue Apr 15 16:44:06 2014 +0200
files: src/Pure/PIDE/document.scala src/Pure/PIDE/text.scala
clarified treatment of markup ranges wrt. revert/convert:
inflate_singularity allows to retrieve information like language_context
more reliably during editing;
That is actually a fundamental change in the markup treatment. It remains
to be seen in the coming weeks/months how it works out compared to
established use over several years.
> What are the drawbacks of a 0s delay?
The extra information by the prover is usually missing: language context,
semantic completion, no_completion flag. With the merge of completion
results in the GUI component, I've found it both theoretically and
practically better to insert the delay by default.
> An alternative would be an incremental filling of the completion popup.
> I think Eclipse does that.
That sounds like even more of an interactive game. Continuous change of
GUI components is now relatively rare in PIDE, after too many problems
coming from it in the past.
> Personally, I like C+SPACE better than C+b as an explicit completion key
If that works for you on your platform it is fine. In general C+SPACE is
very unportable, and often already used by the desktop environment (e.g.
on Mac OS X).
C+b is more likely to work, although hijacking existing jEdit keybindings
is not ideal. I will generally refrain from further ambition in default
key bindings, since there is hardly any free space left in what works
universally. There are just too many different OS platforms, input
methods, national keyboards etc.
> I encountered some behaviour which I found confusing (5b171d4e1d6e):
> theory Scratch imports Main begin
> notepad begin
> If I now enter an "s" after the from, a popup listing possible facts
> appears (which is expected). Close this popup (for example, by pressing
> "Esc"). Now press C+b to open it again. The first suggestions is now
> "sledgehammer (keyword)", which was absent before.
I keep that one for later. The mechanism is already very complex, and not
always predictable, but it might be perfectly normal nonetheless.
More information about the isabelle-dev