Re: [isabelle] signature of ml_antiquotation.ML: inline, value, embedded, etc.

On 12/10/2021 18:51, Kevin Kappelmann wrote:
> Thanks for the hints. I am very well aware of what you call an
> "induction over the sources" and do it all the time. In this particular
> case, however, I got lost because there are no extra headlines and
> chasing down the definitions for the flag "embedded" left me puzzled (I
> stopped at `update_reports` in `antiquote.ML`). I'd find a note about
> the meaning of the flag `embedded` helpful.

There is another meta story behind it that is not explained anywhere, but very
implicit in the history of the past 10 years.

The traditional antiquotation syntax @{name args} stems from the early times
of Isabelle/Isar > 20 years ago.

Approx. 7 years ago, this was refined for control-cartouches:




usually with fancy symbol rendering for the control symbol, e.g. \<^verbatim>
for string literals in Isabelle/ML (or verbatim text in LaTeX documents).

The "embedded" antiquotations prefer this syntax, with formal markup to update
sources via "isabelle update_cartouches". Thus there is a chance to
discontinue the old antiquotation syntax eventually. (But that will require to
change syntax e.g. for @{thms} or @{lemma}).

There will be more such "embedded" forms in other sublanguages of Isabelle
without the old antiquote syntax. E.g. in inner syntax (types and terms).


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.