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
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
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) (Symbol.explode name)) 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
|
