On Fri, 21 Feb 2014, Makarius wrote:
* Improved completion based on context information about embedded
languages: keywords are only completed for outer syntax, symbols for
languages that support them. E.g. no symbol completion for ML source,
but within ML strings, comments, antiquotations.
This refers to Isabelle/5ff4742f27ec. No more accidental symbol completion
of "fn x => x" in ML! (Many years ago someone proposed an opportunistic
change the ML syntax to avoid this annoyance). Similar for Isabelle document
sources, with latex macros etc. Consequently the option
jedit_completion_immediate may be used more aggresively.
This is gradually improving further, now at Isabelle/945ad7eaf37f.
Notably:
* "`" produces a completion popup for a text cartouche, even though it
remains to be seen where it gets actually used apart from the @{rail}
antiquotation.
* "@{" completes to a closed antiquotation with the caret at the proper
spot to continue. Proof General users may have to unlearn C-c C-a C-a
and get used to clear text completion (with semantic language
context).
Moreover:
* Semantic completion, based on failed name space lookups produced by
the prover. E.g. after typing
ML {* @{t} *}
with the curser touching the "t", there will be a red box to indicate
the possibility to use explicit C+b completion from this semantic
information.
This works for all newer mechanisms that use Name_Space.check, instead of
the old form Name_Space.intern followed by manual table lookup.
Unfortunately, the most interesting name space, the one of facts, is still
a bit convoluted, and I need to find ways to retrofit it into that model.
(As usual the actual mechanism is easier to implement, than working
through thick sediments of slight oddities in the system to make it all
work in practice.)
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
