Re: [isabelle] Symbol Shortcuts vs. LaTeX code

On Wed, 30 Apr 2014, Joachim Breitner wrote:

Am Montag, den 28.04.2014, 11:03 +0200 schrieb Joachim Breitner:
Is there maybe a way of entering a \ that prevents a following auto
completion? I tried “\\cite” (which would be a way that I would have
discovered without reading documentation), but that does not work.

a quite horrible workaround is adding

\catcode`\|=0 %

to your preamble, and then simply write your LaTeX commands with |
instead of \. It will break any real occurrence of | in the code and
look really strange, but at least your workflow is uninterrupted. If |
is not good, other characters might work.

Low-level TeX hacking is normally not necessary in the Isabelle document preparation system -- we stopped doing that 15 years ago.

Milner's meta-language is better suited for document programming than Knuth's macro-language, i.e. you just make your own document antiquotation @{cite NAME} with Isabelle syntax.

Just do a hypersearch for Thy_Output.antiquotation over all .ML and .thy files of the Isabelle distribution to get some ideas. $ISABELLE_HOME/src/Pure/Thy/rail.ML is a notable example that does *not* pretty print formal entities, but emits LaTeX macros directly.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.