Email Gateway (Aug 23 2022 at 08:11): Email Gateway (Aug 23 2022 at 08:11):From: Walther Neuper <walther.neuper@jku.at>
What is the simplest way to latex ML code
ML <
(e.g.)
fun fff 1 = 1
| fff 2 = 2
| fff n = n
>
such that the surrounding "ML <" and ">" disappear. Presently I use
(<)ML(>) <
(e.g.)
fun fff 1 = 1
| fff 2 = 2
| fff n = n
>
which hides the "ML" but not "<" and ">". I also studied
~~/src/Doc/Implementation/* but would like to avoid the huge overhead.
Many thanks in advance for any help,
Walther
Email Gateway (Aug 23 2022 at 08:59):From: Makarius <makarius@sketis.net>
The meaning of Isabelle document output is defined by the generated LaTeX
source. Attached is my solution to the problem, after looking carefully at the
generated macros.
The core of it is as follows:
\renewcommand{\isatagML}{%
\begingroup%
\isabellestyle{tt}\isastyle%
\def\isacommand##1{\relax}%
\def\isacartoucheopen{\relax}%
\def\isacartoucheclose{\relax}%
}
\renewcommand{\endisatagML}{\endgroup}
Note that nothing special is done about whitespace: you need to write the
original source carefully, such that the effective spacing comes out in the
way you intend.
Makarius
Test_ML.tar.gz
Email Gateway (Aug 23 2022 at 09:00):From: Walther Neuper <walther.neuper@jku.at>
On 20.04.20 21:58, Makarius wrote:
The meaning of Isabelle document output is defined by the generated LaTeX
source. Attached is my solution to the problem, after looking carefully at the
generated macros.The core of it is as follows:
\renewcommand{\isatagML}{%
\begingroup%
\isabellestyle{tt}\isastyle%
\def\isacommand##1{\relax}%
\def\isacartoucheopen{\relax}%
\def\isacartoucheclose{\relax}%
}
\renewcommand{\endisatagML}{\endgroup}
Thank you very much for this solution! Will be used soon.
Walther
Note that nothing special is done about whitespace: you need to write the
original source carefully, such that the effective spacing comes out in the
way you intend.Makarius
Last updated: Apr 25 2024 at 12:23 UTC