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, 126 insertions, 0 deletions

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