1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
|
# 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!
|
