[isabelle-dev] @ML antiquotation in generated code

[Johannes Hölzl]

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?

 - Johannes