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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
