[isabelle-dev] @ML antiquotation in generated code

Makarius makarius at sketis.net
Mon Oct 20 17:55:37 CEST 2014

On Thu, 9 Oct 2014, Johannes Hölzl wrote:

> In 3094b0edd6b5 I needed to change a document comment {* ..*} to a
> source comment (* .. *). Looks like using the @{ML ..} antiquotation in
> a document comment does not work. Latex does not allow \verb inside
> commands-parameters.
> Is it possible to change \verb to \texttt, with the necessary _ -> \_
> and maybe more conversions?

I have reworked this in Isabelle/23a380cc45f4, with the following NEWS 

*** Document preparation ***

* Official support for "tt" style variants, via \isatt{...} or
\begin{isabellett}...\end{isabellett}. The somewhat fragile \verb or
verbatim environment of LaTeX is no longer used. This allows @{ML} etc.
as argument to other macros (such as footnotes).

* Document antiquotation @{verbatim} prints ASCII text literally in "tt"

This means, the @{verbatim} antiquotation is no longer retricted to 
applications in $ISABELLE_HOME/src/Doc/.

In ac4f764c5be1, I have already reverted your change 3094b0edd6b5.



More information about the isabelle-dev mailing list