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