HOL-Theorem-Prover
HOL munger should not translate inside LaTeX comments
The built-in lexer should know when it has just passed over a %... On the other hand, having to spot that it's inside a verbatim type environment is a very hard prospect.
Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.
Actually, if users are just forbidden from using verbatim, this wouldn't be so bad. Inside an alltt they can use \% to get a % that isn't stripped as a comment by the munger. Percent signs inside a \verb remain a problem, but I guess that usage is pretty uncommon.
Encountered the same issue. HOL munger would produce output which would be displayed in the PDF despite the relevant statement being inside a comment. Workaround: mangle the command so that it cannot be understood by the HOL munger, but it's still obvious what the intent is after the code is uncommented
