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

[Lars Noschinski]

On 31.03.2014 22:04, Makarius wrote:

I played a bit around with your new completion setup.
>   - Support for semantic completion based on failed name space lookup.
>     The error produced by the prover contains information about
>     alternative names that are accessible in a particular position.
>     This may be used with explicit completion (C+b) or implicit
>     completion after some delay.
Where C+b is bound to "Complete Isabelle text", I assume (following the
repository versions, it was still "Complete Word" for me).

>   - 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. I also noticed that "__" is marked as completable, but you
need to request explicit completion -- is this intended?
>   - 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.

What are the drawbacks of a 0s delay? The one I could observe is that I
need to requeste fact completion explicitly, which is okay-ish for me --
I often need to think about the right facts anyway. An alternative would
be an incremental filling of the completion popup. I think Eclipse does
that.

Personally, I like C+SPACE better than C+b as an explicit completion key
binding.

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.

 -- Lars