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.

5 files changed, 236 insertions, 0 deletions

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..e0f0498
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,2 @@
+output/*
+*~
diff --git a/Latex.thy b/Latex.thy
new file mode 100644
index 0000000..81f582d
--- /dev/null
+++ b/Latex.thy
@@ -0,0 +1,126 @@
+theory Latex imports
+ Main
+keywords
+ "export_snippets" :: thy_decl
+begin  
+
+text \<open>
+
+Usage: invoke @{command export_snippets} in theories you want
+to generate snippets of. They will end up in the document output;
+you might need sth like @{verbatim "-e *:document/snippets.tex"} on
+@{verbatim "isabelle build"}.
+
+Otherwise, find the output under @{verbatim "isabelle-export:"}
+in the file browser panel.
+\<close>
+
+ML \<open>
+
+fun export_snippet searchterm lthy = Thy_Info.add_presentation (fn {options, segments, ...} => fn thy => 
+  let
+    val keywords = Thy_Header.get_keywords thy;
+    val thy_name = Context.theory_base_name thy;
+
+    val segments_grouped = fold
+      (fn s => fn a::acc => if Toplevel.is_proof (#prev_state s)
+        then (a @ [s]) :: acc else [s] :: a :: acc) (tl segments) [[hd segments]]
+    |> rev
+    |> filter (fn segments => not (Toplevel.is_ignored (#command (hd segments))))
+
+    val segments_filtered = if searchterm = "" then segments_grouped else
+      filter (fn segments => Toplevel.name_of (#command (hd segments)) = searchterm) segments_grouped;
+
+    val segment_names = segments_filtered
+      |> map (fn segments =>
+        let
+          val {span, command,...} = hd segments
+          val nonblank = filter (not o Token.is_space) (Command_Span.content span)
+          val name = case nonblank of
+              _ :: name :: _ => Token.content_of name
+            | _ => ""
+          val symbols = name
+            |> Symbol.explode
+            |> map (fn sym => 
+                 if Symbol.is_ascii_letter sym orelse Symbol.is_ascii_digit sym 
+                 then sym else if Symbol.is_printable sym then "-" else "")
+          val looks_like_name = not (exists (Symbol.is_blank) symbols) andalso length symbols <> 0;
+          val command_name = Toplevel.name_of command
+        in (not looks_like_name, command_name ^ ":" ^ (if looks_like_name then String.concat symbols else "")) end);
+
+    val markup = segments_filtered
+      |> map (fn segments =>
+           SOME (YXML.parse_body (XML.content_of (Scan.catch (Document_Output.present_thy options keywords thy_name) segments)))
+           handle Fail _ => NONE)
+
+    fun render_macro_lines snippet_name stack n kind attrs trees = 
+      case AList.lookup (op =) attrs "name" of
+      SOME name =>
+        let 
+          val macro = "isa" ^ kind ^ name ^ "\n";
+          val (n', content) = fold (fn t => fn (n, ts) =>
+             let val (n', t) = render_lines snippet_name (macro :: stack) n t
+             in (n', t::ts) end) trees (n,[])
+        in if name = "invisible" then (n,"") else (n', "\\" ^ macro 
+           ^ String.concat (rev content)
+           ^ "\\end" ^ macro) 
+        end
+      | NONE => error "terru misunderstood the YXML"
+    and render_lines snippet_name stack n (XML.Text str) = 
+         let
+           val chunks = Metis_Useful.split "\\isanewline\n" str;
+           val n' = length chunks;
+           val breaker = fn n => fold (fn m => fn acc => "%\n\\end" ^ m ^ acc ^ "\\" ^ m) 
+                  stack ("\\isanewline}%\n\\SNIP{" ^ snippet_name ^ "-" ^ string_of_int n ^ "}{%\n");
+           val broken = chunks
+             |> map_index (fn (i, a) => if i = length chunks - 1 then a else a ^ breaker (1+i+n));
+         in (n+n'-1, String.concat broken) end
+      | render_lines snippet_name stack n (XML.Elem ((name, attrs), trees)) =  case name of
+           "latex_delim" => render_macro_lines snippet_name stack n "delim" attrs trees
+         | "latex_tag" => render_macro_lines snippet_name stack n "tag" attrs trees
+         | tag =>
+            let
+              val _ = warning ("unknown markup tag " ^ tag);
+              val (n', content) = fold (fn t => fn (n, ts) =>
+                let val (m, t) = render_lines snippet_name stack n t
+                in (m, t::ts) end) trees (n,[]);
+            in (n', String.concat (rev content)) end
+    val snippets = markup
+      |> Metis_Useful.zip segment_names (* why is this only in metis ?? *)
+      |> map_filter (fn ((needs_hash, name), SOME texchunks) => 
+          if length texchunks > 0 (* otherwise only header/footer, no content *)
+          then let 
+             val snippet_name = if needs_hash then let val hash = XML.content_of texchunks
+               |> (SHA1.rep o SHA1.digest)
+               |> Symbol.explode
+               |> take 6
+               |> String.concat
+              in name ^ hash end else name
+             val (_, latex) = fold (fn chunk => fn (n, lines) => 
+                 let val (n', content) = render_lines snippet_name [] n chunk
+                 in (n', content::lines) end) (( texchunks)) (0,[])
+             val body = String.concat (rev latex)
+               |> unprefix "%\n\\begin{isabellebody}%\n"
+               |> unsuffix "%\n\\end{isabellebody}%\n"
+            in SOME ("\\SNIP{" ^ snippet_name ^ "-0" ^ "}{%\n" ^ body ^ "}%\n") end
+          else NONE 
+        | (_, NONE) => NONE)
+    val binding = \<^path_binding>\<open>snippets\<close>
+      |> Path.map_binding (fn dir => Path.append dir (Path.basic ("snippets_"^thy_name^".tex")))
+  in
+    Export.export thy binding (map XML.Text (snippets))
+  end
+) lthy;
+
+val _ =
+  Outer_Syntax.local_theory \<^command_keyword>\<open>export_snippets\<close> "export LaTeX snippet"
+    (Scan.optional Parse.string "" >> (fn name =>
+       Local_Theory.background_theory (fn thy => (
+         writeln (Export.message thy (Path.basic "snippets"));
+         export_snippet name thy))));
+
+\<close>
+
+export_snippets
+
+end
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!
diff --git a/ROOT b/ROOT
new file mode 100644
index 0000000..c2e8e43
--- /dev/null
+++ b/ROOT
@@ -0,0 +1,6 @@
+session "isabelle-snippets" = HOL +
+  options [document = pdf, document_output = "output"]
+  theories [document = false]
+    Latex
+  document_files
+    "root.tex"
diff --git a/document/root.tex b/document/root.tex
new file mode 100644
index 0000000..1dec5fa
--- /dev/null
+++ b/document/root.tex
@@ -0,0 +1,60 @@
+\documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
+\usepackage{isabelle,isabellesym}
+
+% further packages required for unusual symbols (see also
+% isabellesym.sty), use only when needed
+
+%\usepackage{amssymb}
+  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
+  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
+  %\<triangleq>, \<yen>, \<lozenge>
+
+%\usepackage{eurosym}
+  %for \<euro>
+
+%\usepackage[only,bigsqcap,bigparallel,fatsemi,interleave,sslash]{stmaryrd}
+  %for \<Sqinter>, \<Parallel>, \<Zsemi>, \<Parallel>, \<sslash>
+
+%\usepackage{eufrak}
+  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
+
+%\usepackage{textcomp}
+  %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
+  %\<currency>
+
+% this should be the last package used
+\usepackage{pdfsetup}
+
+% urls in roman style, theory text in math-similar italics
+\urlstyle{rm}
+\isabellestyle{it}
+
+% for uniform font size
+%\renewcommand{\isastyle}{\isastyleminor}
+
+
+\begin{document}
+
+\title{isabelle-snippets}
+\author{terru}
+\maketitle
+
+\tableofcontents
+
+% sane default for proof documents
+\parindent 0pt\parskip 0.5ex
+
+% generated text of all theories
+\input{session}
+
+% optional bibliography
+%\bibliographystyle{abbrv}
+%\bibliography{root}
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End: