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