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