This is too late for the carnival and two early for the 1st of April, but
here it is nonetheless ...
In ef2ffd622264 from a few days ago, the "style" slot of document
antiquotations has become subject to the standard name space policies,
which means it participates in formal PIDE markup and semantic completion
for free.
For example, consider this piece of text in Isabelle/jEdit:
text {* @{term (__) "x"} *}
with the cursor after the universal wildcard "__". This gives a
completion popup that reveals the full name space content of these formal
entities of kind "antiquotation style".
That is not just silly, since the changeset above shows how to do it in a
small application that is not as complex as the facts name space. The ML
source after the change is actually a bit simpler than before, because
error handling is already included in the name space table operations
(which are authentic and strict).
Of course, it is also possible to leave the "term" name above open, and
use "__" or "t_" or whatever to explore the possibilities.
Another example is this mostly empty template:
text {* @{__ (__) __} *}
it allows to explore each slot consecutively, assuming that the basic
syntax outline is already correct.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
