equal
deleted
inserted
replaced
27 | clean_name "." = "dot" |
27 | clean_name "." = "dot" |
28 | clean_name "_" = "underscore" |
28 | clean_name "_" = "underscore" |
29 | clean_name "{" = "braceleft" |
29 | clean_name "{" = "braceleft" |
30 | clean_name "}" = "braceright" |
30 | clean_name "}" = "braceright" |
31 | clean_name s = s |> translate_string (fn "_" => "-" | c => c); |
31 | clean_name s = s |> translate_string (fn "_" => "-" | c => c); |
32 |
|
33 val str_of_source = space_implode " " o map OuterLex.unparse o #2 o #1 o Args.dest_src; |
|
34 |
|
35 fun tweak_line s = |
|
36 if ! O.display then s else Symbol.strip_blanks s; |
|
37 |
|
38 val pretty_text = Pretty.chunks o map Pretty.str o map tweak_line o Library.split_lines; |
|
39 |
|
40 fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t; |
|
41 fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of; |
|
42 |
32 |
43 |
33 |
44 (* verbatim text *) |
34 (* verbatim text *) |
45 |
35 |
46 val verbatim = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|"; |
36 val verbatim = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|"; |
76 val txt' = if kind = "" then txt else kind ^ " " ^ txt; |
66 val txt' = if kind = "" then txt else kind ^ " " ^ txt; |
77 val _ = writeln (ml (txt1, txt2)); |
67 val _ = writeln (ml (txt1, txt2)); |
78 val _ = ML_Context.eval_in (SOME ctxt) false Position.none (ml (txt1, txt2)); |
68 val _ = ML_Context.eval_in (SOME ctxt) false Position.none (ml (txt1, txt2)); |
79 in |
69 in |
80 "\\indexml" ^ kind ^ enclose "{" "}" (clean_string txt1) ^ |
70 "\\indexml" ^ kind ^ enclose "{" "}" (clean_string txt1) ^ |
81 ((if ! O.source then str_of_source src else txt') |
71 ((if ! O.source then ThyOutput.str_of_source src else txt') |
82 |> (if ! O.quotes then quote else I) |
72 |> (if ! O.quotes then quote else I) |
83 |> (if ! O.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}" |
73 |> (if ! O.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}" |
84 else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n")) |
74 else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n")) |
85 end; |
75 end; |
86 |
76 |
110 (* theorems with names *) |
100 (* theorems with names *) |
111 |
101 |
112 local |
102 local |
113 |
103 |
114 fun output_named_thms src ctxt xs = |
104 fun output_named_thms src ctxt xs = |
115 map (apfst (pretty_thm ctxt)) xs (*always pretty in order to exhibit errors!*) |
105 map (apfst (ThyOutput.pretty_thm ctxt)) xs (*always pretty in order to exhibit errors!*) |
116 |> (if ! O.quotes then map (apfst Pretty.quote) else I) |
106 |> (if ! O.quotes then map (apfst Pretty.quote) else I) |
117 |> (if ! O.display then |
107 |> (if ! O.display then |
118 map (fn (p, name) => |
108 map (fn (p, name) => |
119 Output.output (Pretty.string_of (Pretty.indent (! O.indent) p)) ^ |
109 Output.output (Pretty.string_of (Pretty.indent (! O.indent) p)) ^ |
120 "\\rulename{" ^ Output.output (Pretty.str_of (pretty_text name)) ^ "}") |
110 "\\rulename{" ^ Output.output (Pretty.str_of (ThyOutput.pretty_text name)) ^ "}") |
121 #> space_implode "\\par\\smallskip%\n" |
111 #> space_implode "\\par\\smallskip%\n" |
122 #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" |
112 #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" |
123 else |
113 else |
124 map (fn (p, name) => |
114 map (fn (p, name) => |
125 Output.output (Pretty.str_of p) ^ |
115 Output.output (Pretty.str_of p) ^ |
126 "\\rulename{" ^ Output.output (Pretty.str_of (pretty_text name)) ^ "}") |
116 "\\rulename{" ^ Output.output (Pretty.str_of (ThyOutput.pretty_text name)) ^ "}") |
127 #> space_implode "\\par\\smallskip%\n" |
117 #> space_implode "\\par\\smallskip%\n" |
128 #> enclose "\\isa{" "}"); |
118 #> enclose "\\isa{" "}"); |
129 |
119 |
130 in |
120 in |
131 |
121 |