diff options
Diffstat (limited to '')
| -rw-r--r-- | Latex.thy | 126 |
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 |