Marginal comments (
\<comment>) normally are part of the LaTeX/PDF output, but are left out when they appear after
text (and some other markup commands I have tried).
term A \<comment> \<open>Marginal comments should appear in LaTeX, right?\<close> text\<open>But apparently not after markup commands.\<close> \<comment> \<open>I'm invisible!\<close>
Is this intended behavior?
Sounds like it's not intended. It's best to report such things directly to the isabelle-users mailing list. This is something Makarius should know about, and he doesn't read Zulip.
Max Jakobitsch has marked this topic as resolved.
Last updated: Aug 15 2022 at 04:16 UTC