Dear Isabelle developers,
I was just found guilty of repeating a mistake that I sadly perpetrate
every now and then when writing markup commands in Isabelle theories.
This is not intentional of my part and I would like to start a
discussion about ways this could be avoided in the future. Maybe I am
not the only one in this situation.
Consider the following example markup command.
text ‹Compactness of @{term entails} implies that Red_I and Red_F are
equivalent to ...›
No warning or error in Isabelle/jEdit nor when building the (AFP in this
case) entry with "isabelle build -c -d $AFP -B Entry_Name". Only later
when building the corresponding document with "-o document" option does
an error is (rightfully) reported. e.g.
Latex error (line N of "File.thy"):
Missing $ inserted.
<inserted text>
$
...harparenright}{\kern0pt}} implies that Red_
Latex error (line N of "File.thy"):
Missing $ inserted.
<inserted text>
$
\end{isamarkuptext}
Knowing that there is an error on this line, I immediately noticed that
I used unescaped underscores, which is now allowed in LaTeX. Here, the
solution was, as often, to use proper antiquotation, i.e., @{const
Red_I} and @{const Red_F}.
I believe that reporting this situation as soon as possible would be
beneficial for the user experience and could help minimize unfortunate
mistakes such as inadvertently pushing changesets that fail when
building documents. One could also argue that it wastes CPU cycles and
time to build the full entry, fail building the document, correct the
text, rebuild the entry, and finally build the full document.
Would it be possible for Isabelle to check for unescaped underscores in
markup commands and report a warning of incompatibility with LaTeX?
Regards,
Martin Desharnais
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
