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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
