author | wenzelm |
Sat, 29 May 2004 15:06:42 +0200 | |
changeset 14835 | 695ee8ad0bb6 |
parent 14776 | 4f3b383a46ae |
child 14899 | d9b6c81b52ac |
permissions | -rw-r--r-- |
9140 | 1 |
(* Title: Pure/Isar/isar_output.ML |
2 |
ID: $Id$ |
|
3 |
Author: Markus Wenzel, TU Muenchen |
|
4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
5 |
||
6 |
Isar theory output. |
|
7 |
*) |
|
8 |
||
9 |
signature ISAR_OUTPUT = |
|
10 |
sig |
|
10321 | 11 |
val add_commands: (string * (Args.src -> Toplevel.state -> string)) list -> unit |
9140 | 12 |
val add_options: (string * (string -> (unit -> string) -> unit -> string)) list -> unit |
9220 | 13 |
val print_antiquotations: unit -> unit |
9140 | 14 |
val boolean: string -> bool |
15 |
val integer: string -> int |
|
16 |
val args: (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list)) -> |
|
10321 | 17 |
(Args.src -> Proof.context -> 'a -> string) -> Args.src -> Toplevel.state -> string |
9140 | 18 |
datatype markup = Markup | MarkupEnv | Verbatim |
19 |
val interest_level: int ref |
|
11714 | 20 |
val modes: string list ref |
12939 | 21 |
val eval_antiquote: Scan.lexicon -> Toplevel.state -> string * Position.T -> string |
9140 | 22 |
val parse_thy: (markup -> OuterLex.token list -> OuterLex.token * OuterLex.token list) -> |
23 |
Scan.lexicon -> Toplevel.transition list -> (OuterLex.token, 'a) Source.source -> |
|
24 |
(Toplevel.transition * (Toplevel.state -> Buffer.T -> Buffer.T)) list * Buffer.T |
|
25 |
val display: bool ref |
|
26 |
val quotes: bool ref |
|
9732 | 27 |
val indent: int ref |
9750 | 28 |
val source: bool ref |
11716 | 29 |
val output_with: (Proof.context -> 'a -> Pretty.T) -> Args.src -> |
30 |
Proof.context -> 'a -> string |
|
9140 | 31 |
end; |
32 |
||
33 |
structure IsarOutput: ISAR_OUTPUT = |
|
34 |
struct |
|
35 |
||
36 |
structure T = OuterLex; |
|
37 |
structure P = OuterParse; |
|
38 |
||
39 |
||
40 |
(** maintain global commands **) |
|
41 |
||
42 |
local |
|
43 |
||
44 |
val global_commands = |
|
10321 | 45 |
ref (Symtab.empty: (Args.src -> Toplevel.state -> string) Symtab.table); |
9140 | 46 |
|
47 |
val global_options = |
|
48 |
ref (Symtab.empty: (string -> (unit -> string) -> unit -> string) Symtab.table); |
|
49 |
||
50 |
||
51 |
fun add_item kind (tab, (name, x)) = |
|
52 |
(if is_none (Symtab.lookup (tab, name)) then () |
|
53 |
else warning ("Redefined antiquotation output " ^ kind ^ ": " ^ quote name); |
|
54 |
Symtab.update ((name, x), tab)); |
|
55 |
||
56 |
fun add_items kind xs tab = foldl (add_item kind) (tab, xs); |
|
57 |
||
58 |
in |
|
59 |
||
60 |
val add_commands = Library.change global_commands o (add_items "command"); |
|
61 |
val add_options = Library.change global_options o (add_items "option"); |
|
62 |
||
63 |
fun command src = |
|
64 |
let val ((name, _), pos) = Args.dest_src src in |
|
65 |
(case Symtab.lookup (! global_commands, name) of |
|
66 |
None => error ("Unknown antiquotation command: " ^ quote name ^ Position.str_of pos) |
|
12881 | 67 |
| Some f => transform_failure (curry Antiquote.ANTIQUOTE_FAIL (name, pos)) (f src)) |
9140 | 68 |
end; |
69 |
||
70 |
fun option (name, s) f () = |
|
71 |
(case Symtab.lookup (! global_options, name) of |
|
72 |
None => error ("Unknown antiquotation option: " ^ quote name) |
|
73 |
| Some opt => opt s f ()); |
|
74 |
||
75 |
fun options [] f = f |
|
76 |
| options (opt :: opts) f = option opt (options opts f); |
|
77 |
||
9213 | 78 |
|
9220 | 79 |
fun print_antiquotations () = |
80 |
[Pretty.big_list "antiquotation commands:" (map Pretty.str (Symtab.keys (! global_commands))), |
|
81 |
Pretty.big_list "antiquotation options:" (map Pretty.str (Symtab.keys (! global_options)))] |
|
82 |
|> Pretty.chunks |> Pretty.writeln; |
|
9213 | 83 |
|
9140 | 84 |
end; |
85 |
||
86 |
||
87 |
||
88 |
(** syntax of antiquotations **) |
|
89 |
||
90 |
(* option values *) |
|
91 |
||
92 |
fun boolean "" = true |
|
93 |
| boolean "true" = true |
|
94 |
| boolean "false" = false |
|
95 |
| boolean s = error ("Bad boolean value: " ^ quote s); |
|
96 |
||
97 |
fun integer s = |
|
98 |
let |
|
99 |
fun int ss = |
|
14835 | 100 |
(case Library.read_int ss of (i, []) => i | _ => error ("Bad integer value: " ^ quote s)); |
9140 | 101 |
in (case Symbol.explode s of "-" :: ss => ~ (int ss) | ss => int ss) end; |
102 |
||
103 |
||
104 |
(* args syntax *) |
|
105 |
||
106 |
fun syntax (scan: (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list))) = |
|
107 |
Args.syntax "antiquotation" scan; |
|
108 |
||
10321 | 109 |
fun args scan f src state : string = |
110 |
let val (ctxt, x) = syntax scan src (Toplevel.context_of state) |
|
111 |
in f src ctxt x end; |
|
9140 | 112 |
|
113 |
||
114 |
(* outer syntax *) |
|
115 |
||
116 |
local |
|
117 |
||
118 |
val property = P.xname -- Scan.optional (P.$$$ "=" |-- P.!!! P.xname) ""; |
|
119 |
val properties = Scan.optional (P.$$$ "[" |-- P.!!! (P.enum "," property --| P.$$$ "]")) []; |
|
120 |
||
121 |
val antiq = P.position P.xname -- properties -- P.arguments --| Scan.ahead P.eof |
|
122 |
>> (fn (((x, pos), y), z) => (y, Args.src ((x, z), pos))); |
|
123 |
||
124 |
fun antiq_args_aux keyword_lexicon (str, pos) = |
|
125 |
Source.of_string str |
|
126 |
|> Symbol.source false |
|
127 |
|> T.source false (K (keyword_lexicon, Scan.empty_lexicon)) pos |
|
128 |
|> T.source_proper |
|
129 |
|> Source.source T.stopper (Scan.error (Scan.bulk (P.!!! antiq))) None |
|
130 |
|> Source.exhaust; |
|
131 |
||
132 |
in |
|
133 |
||
134 |
fun antiq_args lex (s, pos) = |
|
135 |
(case antiq_args_aux lex (s, pos) of [x] => x | _ => raise ERROR) handle ERROR => |
|
136 |
error ("Malformed antiquotation: " ^ quote ("@{" ^ s ^ "}") ^ Position.str_of pos); |
|
137 |
||
138 |
end; |
|
139 |
||
140 |
||
141 |
(* eval_antiquote *) |
|
142 |
||
11714 | 143 |
val modes = ref ([]: string list); |
144 |
||
9140 | 145 |
fun eval_antiquote lex state (str, pos) = |
146 |
let |
|
147 |
fun expand (Antiquote.Text s) = s |
|
148 |
| expand (Antiquote.Antiq x) = |
|
149 |
let val (opts, src) = antiq_args lex x in |
|
10739 | 150 |
options opts (fn () => command src state) (); (*preview errors!*) |
11714 | 151 |
Library.setmp print_mode (! modes @ Latex.modes @ ! print_mode) |
10570 | 152 |
(options opts (fn () => command src state)) () |
10321 | 153 |
end; |
9140 | 154 |
val ants = Antiquote.antiquotes_of (str, pos); |
155 |
in |
|
156 |
if Toplevel.is_toplevel state andalso exists Antiquote.is_antiq ants then |
|
157 |
error ("Cannot expand antiquotations at top-level" ^ Position.str_of pos) |
|
158 |
else implode (map expand ants) |
|
159 |
end; |
|
160 |
||
161 |
||
162 |
||
163 |
(** present theory source **) |
|
164 |
||
165 |
(* present_tokens *) |
|
166 |
||
167 |
val interest_level = ref 0; |
|
168 |
||
11861 | 169 |
fun present_tokens lex (flag, toks) state = |
170 |
Buffer.add (case flag of None => "" | Some b => Latex.flag_markup b) o |
|
171 |
(toks |
|
172 |
|> mapfilter (fn (tk, i) => if i > ! interest_level then None else Some tk) |
|
173 |
|> map (apsnd (eval_antiquote lex state)) |
|
174 |
|> Latex.output_tokens |
|
175 |
|> Buffer.add); |
|
9140 | 176 |
|
177 |
||
178 |
(* parse_thy *) |
|
179 |
||
180 |
datatype markup = Markup | MarkupEnv | Verbatim; |
|
181 |
||
182 |
local |
|
183 |
||
184 |
val opt_newline = Scan.option (Scan.one T.is_newline); |
|
185 |
||
186 |
fun check_level i = |
|
187 |
if i > 0 then Scan.succeed () |
|
188 |
else Scan.fail_with (K "Bad nesting of meta-comments"); |
|
189 |
||
190 |
val ignore = |
|
13775
a918c547cd4d
corrected swallowing of newlines after end-of-ignore: rollback
oheimb
parents:
13774
diff
changeset
|
191 |
Scan.depend (fn i => opt_newline |-- P.position (Scan.one T.is_begin_ignore) >> pair (i + 1)) || |
a918c547cd4d
corrected swallowing of newlines after end-of-ignore: rollback
oheimb
parents:
13774
diff
changeset
|
192 |
Scan.depend (fn i => P.position (Scan.one T.is_end_ignore) --| |
13774
77a1e723151d
corrected swallowing of newlines after end-of-ignore (improved)
oheimb
parents:
13742
diff
changeset
|
193 |
(opt_newline -- check_level i) >> pair (i - 1)); |
9140 | 194 |
|
195 |
val ignore_cmd = Scan.state -- ignore |
|
11861 | 196 |
>> (fn (i, (x, pos)) => (false, (None, ((Latex.Basic x, ("", pos)), i)))); |
9140 | 197 |
|
198 |
||
199 |
val is_improper = not o (T.is_proper orf T.is_begin_ignore orf T.is_end_ignore); |
|
200 |
val improper = Scan.any is_improper; |
|
201 |
||
202 |
val improper_keep_indent = Scan.repeat |
|
203 |
(Scan.unless (Scan.one T.is_indent -- Scan.one T.is_proper) (Scan.one is_improper)); |
|
204 |
||
205 |
val improper_end = |
|
206 |
(improper -- P.semicolon) |-- improper_keep_indent || |
|
207 |
improper_keep_indent; |
|
208 |
||
209 |
||
210 |
val stopper = |
|
11861 | 211 |
((false, (None, ((Latex.Basic (#1 T.stopper), ("", Position.none)), 0))), |
212 |
fn (_, (_, ((Latex.Basic x, _), _))) => (#2 T.stopper x) | _ => false); |
|
9140 | 213 |
|
214 |
in |
|
215 |
||
216 |
fun parse_thy markup lex trs src = |
|
217 |
let |
|
218 |
val text = P.position P.text; |
|
9220 | 219 |
val token = Scan.depend (fn i => |
9140 | 220 |
(improper |-- markup Markup -- P.!!!! (improper |-- text --| improper_end) |
11861 | 221 |
>> (fn (x, y) => (true, (Some true, ((Latex.Markup (T.val_of x), y), i)))) || |
9140 | 222 |
improper |-- markup MarkupEnv -- P.!!!! (improper |-- text --| improper_end) |
11861 | 223 |
>> (fn (x, y) => (true, (Some true, ((Latex.MarkupEnv (T.val_of x), y), i)))) || |
9140 | 224 |
(P.$$$ "--" |-- P.!!!! (improper |-- text)) |
11861 | 225 |
>> (fn y => (false, (None, ((Latex.Markup "cmt", y), i)))) || |
9140 | 226 |
(improper -- markup Verbatim) |-- P.!!!! (improper |-- text --| improper_end) |
11861 | 227 |
>> (fn y => (true, (None, ((Latex.Verbatim, y), i)))) || |
9140 | 228 |
P.position (Scan.one T.not_eof) |
11861 | 229 |
>> (fn (x, pos) => (T.is_kind T.Command x, (Some false, ((Latex.Basic x, ("", pos)), i))))) |
9220 | 230 |
>> pair i); |
9140 | 231 |
|
232 |
val body = Scan.any (not o fst andf not o #2 stopper); |
|
11861 | 233 |
val section = body -- Scan.one fst -- body |
234 |
>> (fn ((b1, c), b2) => (#1 (#2 c), map (snd o snd) (b1 @ (c :: b2)))); |
|
9140 | 235 |
|
236 |
val cmds = |
|
237 |
src |
|
238 |
|> Source.filter (not o T.is_semicolon) |
|
239 |
|> Source.source' 0 T.stopper (Scan.error (Scan.bulk (ignore_cmd || token))) None |
|
240 |
|> Source.source stopper (Scan.error (Scan.bulk section)) None |
|
241 |
|> Source.exhaust; |
|
242 |
in |
|
243 |
if length cmds = length trs then |
|
244 |
(trs ~~ map (present_tokens lex) cmds, Buffer.empty) |
|
11861 | 245 |
else error "Messed-up outer syntax for presentation" |
9140 | 246 |
end; |
247 |
||
248 |
end; |
|
249 |
||
250 |
||
251 |
||
252 |
(** setup default output **) |
|
253 |
||
254 |
(* options *) |
|
255 |
||
256 |
val display = ref false; |
|
257 |
val quotes = ref false; |
|
9732 | 258 |
val indent = ref 0; |
9750 | 259 |
val source = ref false; |
13929
21615e44ba88
Added "break" flag to allow line breaks within \isa{...}
berghofe
parents:
13775
diff
changeset
|
260 |
val break = ref false; |
9140 | 261 |
|
262 |
val _ = add_options |
|
9220 | 263 |
[("show_types", Library.setmp Syntax.show_types o boolean), |
264 |
("show_sorts", Library.setmp Syntax.show_sorts o boolean), |
|
14707 | 265 |
("show_structs", Library.setmp show_structs o boolean), |
14696 | 266 |
("long_names", Library.setmp NameSpace.long_names o boolean), |
9220 | 267 |
("eta_contract", Library.setmp Syntax.eta_contract o boolean), |
9140 | 268 |
("display", Library.setmp display o boolean), |
13929
21615e44ba88
Added "break" flag to allow line breaks within \isa{...}
berghofe
parents:
13775
diff
changeset
|
269 |
("break", Library.setmp break o boolean), |
9140 | 270 |
("quotes", Library.setmp quotes o boolean), |
271 |
("mode", fn s => fn f => fn () => Library.setmp print_mode (s :: ! print_mode) f ()), |
|
9732 | 272 |
("margin", Pretty.setmp_margin o integer), |
9750 | 273 |
("indent", Library.setmp indent o integer), |
10321 | 274 |
("source", Library.setmp source o boolean), |
275 |
("goals_limit", Library.setmp goals_limit o integer)]; |
|
9140 | 276 |
|
277 |
||
278 |
(* commands *) |
|
279 |
||
280 |
fun cond_quote prt = |
|
281 |
if ! quotes then Pretty.quote prt else prt; |
|
282 |
||
283 |
fun cond_display prt = |
|
284 |
if ! display then |
|
14835 | 285 |
Output.output (Pretty.string_of (Pretty.indent (! indent) prt)) |
9863 | 286 |
|> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" |
9140 | 287 |
else |
14835 | 288 |
Output.output ((if ! break then Pretty.string_of else Pretty.str_of) prt) |
9140 | 289 |
|> enclose "\\isa{" "}"; |
290 |
||
14345 | 291 |
fun cond_seq_display prts = |
292 |
if ! display then |
|
14835 | 293 |
map (Output.output o Pretty.string_of o Pretty.indent (! indent)) prts |
14345 | 294 |
|> separate "\\isasep\\isanewline%\n" |
295 |
|> implode |
|
296 |
|> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" |
|
297 |
else |
|
14835 | 298 |
map (Output.output o (if ! break then Pretty.string_of else Pretty.str_of)) prts |
14345 | 299 |
|> separate "\\isasep\\isanewline%\n" |
300 |
|> implode |
|
301 |
|> enclose "\\isa{" "}"; |
|
302 |
||
11011
14b78c0c9f05
pretty_text: tweak_lines handles linebreaks gracefully;
wenzelm
parents:
10739
diff
changeset
|
303 |
fun tweak_line s = |
14b78c0c9f05
pretty_text: tweak_lines handles linebreaks gracefully;
wenzelm
parents:
10739
diff
changeset
|
304 |
if ! display then s else Symbol.strip_blanks s; |
9750 | 305 |
|
11011
14b78c0c9f05
pretty_text: tweak_lines handles linebreaks gracefully;
wenzelm
parents:
10739
diff
changeset
|
306 |
val pretty_text = Pretty.chunks o map Pretty.str o map tweak_line o Library.split_lines; |
9140 | 307 |
|
9750 | 308 |
val pretty_source = |
309 |
pretty_text o space_implode " " o map Args.string_of o #2 o #1 o Args.dest_src; |
|
9140 | 310 |
|
12055 | 311 |
fun pretty_term ctxt = ProofContext.pretty_term ctxt o ProofContext.extern_skolem ctxt; |
9140 | 312 |
|
14345 | 313 |
fun pretty_thm ctxt = pretty_term ctxt o Thm.prop_of; |
9140 | 314 |
|
12055 | 315 |
fun pretty_prf full ctxt thms = (* FIXME context syntax!? *) |
11524
197f2e14a714
Added functions for printing primitive proof terms.
berghofe
parents:
11240
diff
changeset
|
316 |
Pretty.chunks (map (ProofSyntax.pretty_proof_of full) thms); |
197f2e14a714
Added functions for printing primitive proof terms.
berghofe
parents:
11240
diff
changeset
|
317 |
|
9750 | 318 |
fun output_with pretty src ctxt x = |
319 |
let |
|
12055 | 320 |
val prt = pretty ctxt x; (*always pretty in order to catch errors!*) |
9750 | 321 |
val prt' = if ! source then pretty_source src else prt; |
322 |
in cond_display (cond_quote prt') end; |
|
9732 | 323 |
|
14345 | 324 |
fun output_seq_with pretty src ctxt xs = |
325 |
let |
|
326 |
val prts = map (pretty ctxt) xs; (*always pretty in order to catch errors!*) |
|
327 |
val prts' = if ! source then [pretty_source src] else prts; |
|
328 |
in cond_seq_display (map cond_quote prts') end; |
|
329 |
||
10360 | 330 |
fun output_goals main_goal src state = args (Scan.succeed ()) (output_with (fn _ => fn _ => |
331 |
Pretty.chunks (Proof.pretty_goals main_goal (Toplevel.proof_of state |
|
332 |
handle Toplevel.UNDEF => error "No proof state")))) src state; |
|
333 |
||
9140 | 334 |
val _ = add_commands |
14696 | 335 |
[("thm", args Attrib.local_thmss (output_seq_with pretty_thm)), |
9750 | 336 |
("prop", args Args.local_prop (output_with pretty_term)), |
337 |
("term", args Args.local_term (output_with pretty_term)), |
|
14776 | 338 |
("typ", args Args.local_typ_raw (output_with ProofContext.pretty_typ)), |
14696 | 339 |
("text", args (Scan.lift Args.name) (output_with (K pretty_text))), |
10360 | 340 |
("goals", output_goals true), |
14696 | 341 |
("subgoals", output_goals false), |
342 |
("prf", args Attrib.local_thmss (output_with (pretty_prf false))), |
|
343 |
("full_prf", args Attrib.local_thmss (output_with (pretty_prf true)))]; |
|
9140 | 344 |
|
345 |
end; |