On 26/09/2022 16:15, Fabian Huch wrote:
No, the Jenkins / Testboard setup and the ML compiler works. However, the
latex setup of those two entries does not.
Trying it manually with "isabelle build -o document ..." the error is actually
this:
*** Latex error (line 24 of "PAC_Checker_MLton.tex"):
*** Undefined control sequence.
*** ...\isacharparenleft}{\kern0pt}\isactrlverbatim
*** Failed to build document "document"
So there is something missing in the Isabelle LaTeX styles, which I have now
amended here:
changeset: 76209:e44e044dadb3
user: wenzelm
date: Mon Sep 26 20:40:19 2022 +0200
files: lib/texinputs/isabellesym.sty
description:
provide missing LaTeX macro, e.g. for AFP/PAC_Checker;
The deeper reason for the omission is that \<^verbatim> in formal document
text produces verbatim LaTeX output without a separate macro \isactrlverbatim.
In contrast, the use in Isabelle/ML remains literally visible --- and it was
rarely used so far.
Now that feature of Isabelle/ML got some extra attention, so maybe it will be
used more often in the future.
It works even better than triple-quoted strings in Scala or Python.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
