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, involving lots of manual work - the "Isabelle Snippets" 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 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!