initial snippet generationHEADmain

this is the result of some hacking during off-hours at mgs25, patched
into a mostly-working state. In use for at least one paper already, so
it should hopefully work for most "basic" theories and possibly more
complex ones.

1 files changed, 42 insertions, 0 deletions

diff --git a/README.md b/README.md
new file mode 100644
index 0000000..d9c68b9
--- /dev/null
+++ b/README.md
@@ -0,0 +1,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!