[isabelle-dev] Semantic completion of antiquotation styles

[Makarius]

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