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

[Makarius]

On 10/11/2021 09:20, Martin Desharnais wrote:
> 
> 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.

The problem can be avoided by not thinking in terms of "guilt", "mistake" or
"perpretration". LaTeX is a very fragile language and no amount of precautions
nor tests will change the situation substantially.

Too much testing can also become a problem on its own account, being neither
necessary nor sufficient for a "good" situation. (We have too many
"uninformative green lights" on the planet, and too much obsession in
producing them.)


In your change e5eeaaf2bd5b you claim to have "fixed" a LaTeX failure, but you
also turned the unchecked formal text \<open>wlog_non_Red_F\<close> into
checked @{thm wlog_non_Red_F}, with different output: the thm statement (with
schematic variables) instead of the thm name. You probably intended to say
@{thm [source] ...} here.

Typical LaTeX document errors are actually of that kind, and often remain
undetected for years. There are also situations where gradual changes in the
LaTeX system give a different appearance of the document at a later stage.


In retrospect, I regret to have given so much weight to LaTeX in 1999, when
the Isabelle document system emerged for the first time.


	Makarius