*** Prover IDE -- Isabelle/Scala/jEdit ***
* Improved syntactic and semantic completion mechanism:
- No completion for Isar keywords that have already been recognized
by the prover, e.g. ":" within accepted Isar syntax looses its
meaning as abbreviation for symbol "\<in>".
- Completion context provides information about embedded languages
of Isabelle: keywords are only completed for outer syntax, symbols
or antiquotations for languages that support them. E.g. no symbol
completion for ML source, but within ML strings, comments,
antiquotations.
- 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.
- 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").
- 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.
- Option jedit_completion_immediate may now get used with
jedit_completion_delay > 0, to complete symbol abbreviations
aggressively while benefiting from combined syntactic and semantic
completion.
- Support for simple completion templates (with single
place-holder), e.g. "`" for text cartouche, or "@{" for
antiquotation.
- Improved treatment of completion vs. various forms of jEdit text
selection (multiple selections, rectangular selections,
rectangular selection as "tall caret").
- More reliable treatment of GUI events vs. completion popups: avoid
loosing keystrokes with slow / remote graphics displays.
These cumulative NEWS refer to Isabelle/075397022503. This also marks the
point where my continously shrinking and growing TODO list has reached a
stable state concerning "completion" and the main activity on this part is
finished for now.
The coming weeks and months are the opportunity to figure out minor snags
and missing bits of completion, *before* we embark on the release in
summer. Although it is a slow and painful process for me to make these
things work, my impression is that the "consumption" of such novelties are
even slower and more painful, and very little actual testing happens.
Completion is particularly critical, because it sits right in the main key
event loop of the editor.
Note that the above changes of default options are not pushed onto people
who are hooked on the repository, because the options from
$ISABELLE_HOME_USER take precedence. It is also worth trying variations
like this:
jedit_completion = true
jedit_completion_delay = 0.5
jedit_completion_immediate = true
Thus former ASCII replacement syntax like ==> --> <= etc. become readily
available as quick input method. Moreover it is always possible to use
single letter abbreviations like : ! & | with explicit C+b (without silly
replacements for Isar keywords that the prover has already recognized).
Ultimately, the improved support for multi-selections helps to use
hypersearch on ASCII replacement syntax with C+b replacement -- next time
we do that semantically, as "refactoring" :-)
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
