[isabelle-dev] antiquotations and type_synonyms

[Makarius]

On Thu, 18 Apr 2013, Tobias Nipkow wrote:

> I was under the impression that type synonyms are expanded in typ
> antiquotations, but apparently not, at least not with 30624dab6054. If I write
> @{typ vname} I get "vname", even if vname is a type synonym for string. Maybe it
> has always been like this, but it means that one cannot automatically display
> (in latex) what some type synonym stands for, one has to type it in. Conversely,
> if they were expanded, one could always prevent that with the [source] modifier.
> Any views on this?

The non-expansion of document antiquatation @{typ} goes back to 
8168600e88a5 (03-Aug-2000), which is a few weeks after it was first 
introduced; before it was just expanding abbreviations.  The changeset 
does not give any explanations, so I can only guess that some early users 
of the new mechanism had asked for slightly different behaviour.

For uniformity it would be better to have @{typ} behave like the 'typ' 
command, but I think it is hard to change after so many years -- printed 
documents by users out there will change without further notice.

Note that the [source] option has other impact on the printing, so it is 
better kept apart.


Technically, it is trivial to have an antiquotation that uses Args.typ 
instead of Args.typ_abbrev.  It is just a matter to devise a half-decent 
mechanism to specify that variant, e.g.

   (1) separate antiquotion with different name

   (2) additional antiquotation option

   (3) optional antiquotation argument (similar to the "term style")

   (4) re-interpretation of print mode like "show_abbrevs" for terms

We have accumulated so many ways to do the same thing ...

Option (1) is looks like the most basic and immediate solution, we only 
need a good name for it, e.g. @{typ_expanded}?


 	Makarius