[isabelle-dev] antiquotations and type_synonyms

[Tobias Nipkow]

Thanks for digging into the history and suggesting various extensions. I now
believe that expanding type synonyms is rarely wanted. My use case was the
display of the rhs of a type synonym, say t = "u list". But then one wants to
see "u list", not an expanded version of it (in case "u" contains further
synonyms). This is getting a bit too fine grained.

This may be one of the rationals why @{typ} works the way it does.

Tobias

Am 21/05/2013 13:49, schrieb 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