[isabelle-dev] NEWS: improved syntactic and semantic completion mechanism

[Makarius]

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
> completion.

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:

changeset:   56326:c3d7b3bb2708
user:        wenzelm
date:        Sun Mar 30 21:03:40 2014 +0200
files:       src/Tools/jEdit/etc/options 
src/Tools/jEdit/src/completion_popup.scala
description:
immediate completion even with delay, which is the default according to 
638b29331549;


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:

changeset:   56590:d01d183e84ea
user:        wenzelm
date:        Tue Apr 15 16:44:06 2014 +0200
files:       src/Pure/PIDE/document.scala src/Pure/PIDE/text.scala
description:
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 
> binding.

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
>    from
> ---------------------------------
>
> 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.


 	Makarius