[isabelle-dev] Wish for warning of unescaped underscores in markup commands

[Martin Desharnais]

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