[isabelle-dev] @ML antiquotation in generated code

[Makarius]

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 
entry:


*** 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"
style.


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.


 	Makarius

----------------------------------------------------------------------------
                               http://stop-ttip.org
----------------------------------------------------------------------------