Email Gateway (Aug 18 2022 at 09:44): Email Gateway (Aug 18 2022 at 09:44):From: Jared Davis <jared@cs.utexas.edu>
Hi,
I have a couple questions about the latex conversion process.
Is there a comment syntax other than (* this *) which doesn't show up in the
LaTeX file? I'd like to be able to comment-out big regions of already commented
code, but since (* these *) won't nest, I don't know how to do that.
When I write things like "[| foo |] ==> bar", the latex converter doesn't
seem to change the "[|" into the nice-looking, single symbol form, and similarly
the arrow is left as ==> instead of changing it into \Longrightarrow, etc. Is
there a way to get it to automatically convert these?
Thanks,
Jared
Email Gateway (Aug 18 2022 at 09:44):From: Makarius <makarius@sketis.net>
On Fri, 29 Sep 2006, Jared Davis wrote:
- Is there a comment syntax other than (* this *) which doesn't show
up in the LaTeX file? I'd like to be able to comment-out big regions
of already commented code, but since (* these *) won't nest, I don't
know how to do that.
(* *) do nest as in ML. The only problem is that Emacs / ProofGeneral
might be confused by this. Some versions should work, despite the
misleading font-lock display.
An alternative is to markup LaTeX output to be invisibile, e.g. like this:
text %invisible {* ... *}
Note that {* ... *} does not nest, and the content needs to be legal
source in terms of the document preparation system.
- When I write things like "[| foo |] ==> bar", the latex converter
doesn't seem to change the "[|" into the nice-looking, single symbol
form, and similarly the arrow is left as ==> instead of changing it
into \Longrightarrow, etc. Is there a way to get it to automatically
convert these?
No. The document system merely presents the sources as they are written.
An alternative is to let the system output formal entities using
antiquatations, e.g. @{thm foo} -- here the output is subject to the
xsymbols/latex print mode.
Makarius
Last updated: May 03 2024 at 08:18 UTC