Stream: General

Topic: ✔ `\<comment>` after `text` omitted in LaTeX output

view this post on Zulip Max Jakobitsch (Feb 03 2022 at 17:48):

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?

view this post on Zulip Manuel Eberl (Feb 03 2022 at 18:05):

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.

view this post on Zulip Notification Bot (Feb 03 2022 at 18:14):

Max Jakobitsch has marked this topic as resolved.

Last updated: Apr 19 2024 at 01:05 UTC