# Isabelle LaTeX snippets, in Isabelle

Need to embed some Isabelle code into a LaTeX document without writing your whole
thing in Isabelle? You've come to the right place! (maybe)

Afaict, there's two other ways to include snippets of Isabelle into LaTeX:
 - the "Theory snippets" section in [`sugar.pdf`](https://isabelle.in.tum.de/dist/Isabelle2025/doc/sugar.pdf),
   involving lots of manual work
 - the ["Isabelle Snippets"](https://astahfrom.github.io/cartouches/) utility by
   Asta Halkjær From, which requires no manual work and instead operates on the
   generated whole-theory LaTeX output, making it somewhat brittle

this is a partial re-implementation of the second approach inside Isabelle/ML,
aiming to be a little less brittle.

## Usage

Include this session into yours, import the `Latex` theory, and then issue a call
to `export_snippets` in your theory. It doesn't matter where — LaTeX will always
be generated once the theory is "done", i.e. at the `end` statement which closes
the file (this also means that in Isabelle/jedit, any potential errors will show
up at the `end`, not the `export_snippets`).

After that, the theory exports will include a file containing `\SNIP` definitions
in the same way as with Asta's snippets tool.

## Limitations

Snippets are generated per top-level command and per line, but not (yet?) per
cartouche. Sometimes snippet names might contain doubles, leading to errors
on the LaTeX side, this is still to-be-fixed.

This tool also re-implements a tiny version of logic which in the normal document
generation process is done in Scala, which may well contain errors and/or be a
little too simplistic. It also removes anything tagged as invisible; the usual
export process does not do that, and instead removes it on the LaTeX side using
an old version of the [comment](https://ctan.org/pkg/comment) package bundled
into Isabelle. Since the comment package works by doing funny things with
catcodes (look up how `verbatim` works if you're curious), it breaks in
interesting ways if done inside snippet definitions.

If you use this and encounter strange errors, please tell me about it!