177 |
172 |
178 |
173 |
179 |
174 |
180 (** present theory source **) |
175 (** present theory source **) |
181 |
176 |
182 (* present_tokens *) |
177 (* presentation tokens *) |
183 |
178 |
184 val interest_level = ref 0; |
179 datatype token = |
185 |
180 NoToken |
186 val hide_commands = ref true; |
181 | BasicToken of T.token |
187 val hidden_commands = ref ([] : string list); |
182 | MarkupToken of string * (string * Position.T) |
188 |
183 | MarkupEnvToken of string * (string * Position.T) |
189 fun add_hidden_commands cmds = (hidden_commands := !hidden_commands @ cmds); |
184 | VerbatimToken of string * Position.T; |
190 |
185 |
191 fun is_proof state = (case Toplevel.node_of state of |
186 fun output_token lex state = |
192 Toplevel.Theory _ => false | _ => true) handle Toplevel.UNDEF => false; |
187 let |
193 |
188 val eval = eval_antiquote lex state |
194 fun is_newline (Latex.Basic tk, _) = T.is_newline tk |
189 in |
195 | is_newline _ = false; |
190 fn NoToken => "" |
196 |
191 | BasicToken tok => Latex.output_basic tok |
197 fun is_hidden (Latex.Basic tk, _) = |
192 | MarkupToken (cmd, txt) => Latex.output_markup cmd (eval txt) |
198 T.is_kind T.Command tk andalso T.val_of tk mem !hidden_commands |
193 | MarkupEnvToken (cmd, txt) => Latex.output_markup_env cmd (eval txt) |
199 | is_hidden _ = false; |
194 | VerbatimToken txt => Latex.output_verbatim (eval txt) |
200 |
195 end; |
201 fun filter_newlines toks = (case List.mapPartial |
196 |
202 (fn (tk, i) => if is_newline tk then SOME tk else NONE) toks of |
197 fun basic_token pred (BasicToken tok) = pred tok |
203 [] => [] | [tk] => [tk] | _ :: toks' => toks'); |
198 | basic_token _ _ = false; |
204 |
199 |
205 fun present_tokens lex (flag, toks) state state' = |
200 val improper_token = basic_token (not o T.is_proper); |
206 Buffer.add (case flag of NONE => "" | SOME b => Latex.flag_markup b) o |
201 val comment_token = basic_token T.is_comment; |
207 ((if !hide_commands andalso exists (is_hidden o fst) toks then [] |
202 val blank_token = basic_token T.is_blank; |
208 else if !hide_commands andalso is_proof state then |
203 val newline_token = basic_token T.is_newline; |
209 if is_proof state' then [] else filter_newlines toks |
204 |
210 else List.mapPartial (fn (tk, i) => |
205 |
211 if i > ! interest_level then NONE else SOME tk) toks) |
206 (* command spans *) |
212 |> map (apsnd (eval_antiquote lex state')) |
207 |
213 |> Latex.output_tokens |
208 type command = string * Position.T * string list; (*name, position, tags*) |
214 |> Buffer.add); |
209 type source = (string * token * int) list; (*raw text, token, meta-comment depth*) |
215 |
210 |
216 |
211 datatype span = Span of command * (source * source * source * source) * bool; |
217 (* parse_thy *) |
212 |
|
213 fun make_span cmd src = |
|
214 let |
|
215 fun take_newline (tok :: toks) = |
|
216 if newline_token (#2 tok) then ([tok], toks, true) |
|
217 else ([], tok :: toks, false) |
|
218 | take_newline [] = ([], [], false); |
|
219 val (((src_prefix, src_main), src_suffix1), (src_suffix2, src_appendix, newline)) = |
|
220 src |
|
221 |> take_prefix (improper_token o #2) |
|
222 ||>> take_suffix (improper_token o #2) |
|
223 ||>> take_prefix (comment_token o #2) |
|
224 ||> take_newline; |
|
225 in Span (cmd, (src_prefix, src_main, src_suffix1 @ src_suffix2, src_appendix), newline) end; |
|
226 |
|
227 |
|
228 (* present spans *) |
|
229 |
|
230 local |
|
231 |
|
232 fun err_bad_nesting pos = |
|
233 error ("Bad nesting of commands in presentation" ^ pos); |
|
234 |
|
235 fun edge1 f (x, y) = if_none (Option.map (Buffer.add o f) (if x = y then NONE else x)) I; |
|
236 fun edge2 f (x, y) = if_none (Option.map (Buffer.add o f) (if x = y then NONE else y)) I; |
|
237 |
|
238 val begin_tag = edge2 Latex.begin_tag; |
|
239 val end_tag = edge1 Latex.end_tag; |
|
240 fun open_delim delim e = edge2 Latex.begin_delim e #> delim #> edge2 Latex.end_delim e; |
|
241 fun close_delim delim e = edge1 Latex.begin_delim e #> delim #> edge1 Latex.end_delim e; |
|
242 |
|
243 in |
|
244 |
|
245 fun present_span lex default_tags span state state' |
|
246 (tag_stack, active_tag, newline, buffer, present_cont) = |
|
247 let |
|
248 val present = fold (fn (raw, tok, d) => |
|
249 if d > 0 then I |
|
250 else Buffer.add raw #> Buffer.add (output_token lex state' tok)); |
|
251 |
|
252 val Span ((cmd_name, cmd_pos, cmd_tags), srcs, span_newline) = span; |
|
253 |
|
254 val (tag, tags) = tag_stack; |
|
255 val tag' = |
|
256 (case tag of NONE => [] | SOME tg => [tg]) |
|
257 |> fold OuterKeyword.update_tags cmd_tags |
|
258 |> try hd; |
|
259 |
|
260 val active_tag' = |
|
261 if is_some tag' then tag' |
|
262 else try hd (default_tags cmd_name); |
|
263 val edge = (active_tag, active_tag'); |
|
264 |
|
265 val newline' = |
|
266 if is_none active_tag' then span_newline else newline; |
|
267 |
|
268 val nesting = Toplevel.level state' - Toplevel.level state; |
|
269 val tag_stack' = |
|
270 if nesting = 0 andalso not (Toplevel.is_proof state) then tag_stack |
|
271 else if nesting >= 0 then (tag', replicate nesting tag @ tags) |
|
272 else |
|
273 (case Library.drop (~ nesting - 1, tags) of |
|
274 tgs :: tgss => (tgs, tgss) |
|
275 | [] => err_bad_nesting (Position.str_of cmd_pos)); |
|
276 |
|
277 val buffer' = |
|
278 buffer |
|
279 |> end_tag edge |
|
280 |> close_delim (fst present_cont) edge |
|
281 |> snd present_cont |
|
282 |> open_delim (present (#1 srcs)) edge |
|
283 |> begin_tag edge |
|
284 |> present (#2 srcs); |
|
285 val present_cont' = |
|
286 if newline then (present (#3 srcs), present (#4 srcs)) |
|
287 else (I, present (#3 srcs) #> present (#4 srcs)); |
|
288 in (tag_stack', active_tag', newline', buffer', present_cont') end; |
|
289 |
|
290 fun present_trailer ((_, tags), active_tag, _, buffer, present_cont) = |
|
291 if not (null tags) then err_bad_nesting " at end of theory" |
|
292 else |
|
293 buffer |
|
294 |> end_tag (active_tag, NONE) |
|
295 |> close_delim (fst present_cont) (active_tag, NONE) |
|
296 |> snd present_cont; |
|
297 |
|
298 end; |
|
299 |
|
300 |
|
301 (* present_thy *) |
218 |
302 |
219 datatype markup = Markup | MarkupEnv | Verbatim; |
303 datatype markup = Markup | MarkupEnv | Verbatim; |
220 |
304 |
221 local |
305 local |
222 |
306 |
223 val opt_newline = Scan.option (Scan.one T.is_newline); |
307 val space_proper = |
224 |
308 Scan.one T.is_blank -- Scan.any T.is_comment -- Scan.one T.is_proper; |
225 fun check_level i = |
|
226 if i > 0 then Scan.succeed () |
|
227 else Scan.fail_with (K "Bad nesting of meta-comments"); |
|
228 |
|
229 val ignore = |
|
230 Scan.depend (fn i => opt_newline |-- P.position (Scan.one T.is_begin_ignore) >> pair (i + 1)) || |
|
231 Scan.depend (fn i => P.position (Scan.one T.is_end_ignore) --| |
|
232 (opt_newline -- check_level i) >> pair (i - 1)); |
|
233 |
|
234 val ignore_cmd = Scan.state -- ignore |
|
235 >> (fn (i, (x, pos)) => (false, (NONE, ((Latex.Basic x, ("", pos)), i)))); |
|
236 |
|
237 |
309 |
238 val is_improper = not o (T.is_proper orf T.is_begin_ignore orf T.is_end_ignore); |
310 val is_improper = not o (T.is_proper orf T.is_begin_ignore orf T.is_end_ignore); |
239 val improper = Scan.any is_improper; |
311 val improper = Scan.any is_improper; |
240 |
312 val improper_end = Scan.repeat (Scan.unless space_proper (Scan.one is_improper)); |
241 val improper_keep_indent = Scan.repeat |
313 |
242 (Scan.unless (Scan.one T.is_indent -- Scan.one T.is_proper) (Scan.one is_improper)); |
314 val opt_newline = Scan.option (Scan.one T.is_newline); |
243 |
315 |
244 val improper_end = |
316 val ignore = |
245 (improper -- P.semicolon) |-- improper_keep_indent || |
317 Scan.depend (fn d => opt_newline |-- Scan.one T.is_begin_ignore |
246 improper_keep_indent; |
318 >> pair (d + 1)) || |
247 |
319 Scan.depend (fn d => Scan.one T.is_end_ignore --| |
248 |
320 (if d = 0 then Scan.fail_with (K "Bad nesting of meta-comments") else opt_newline) |
249 val stopper = |
321 >> pair (d - 1)); |
250 ((false, (NONE, ((Latex.Basic (#1 T.stopper), ("", Position.none)), 0))), |
322 |
251 fn (_, (_, ((Latex.Basic x, _), _))) => (#2 T.stopper x) | _ => false); |
323 val tag = (improper -- P.$$$ "%" -- improper) |-- P.!!! (P.tag_name --| improper_end); |
252 |
324 |
253 in |
325 in |
254 |
326 |
255 fun parse_thy markup lex trs src = |
327 fun present_thy lex default_tags is_markup trs src = |
256 let |
328 let |
257 val text = P.position P.text; |
329 (* tokens *) |
258 val token = Scan.peek (fn i => |
330 |
259 (improper |-- markup Markup -- P.!!!! (improper |-- text --| improper_end) |
331 val ignored = Scan.state --| ignore |
260 >> (fn (x, y) => (true, (SOME true, ((Latex.Markup (T.val_of x), y), i)))) || |
332 >> (fn d => (NONE, ("", NoToken, d))); |
261 improper |-- markup MarkupEnv -- P.!!!! (improper |-- text --| improper_end) |
333 |
262 >> (fn (x, y) => (true, (SOME true, ((Latex.MarkupEnv (T.val_of x), y), i)))) || |
334 fun markup flag mark mk = Scan.peek (fn d => |
263 (P.$$$ "--" |-- P.!!!! (improper |-- text)) |
335 improper |-- |
264 >> (fn y => (false, (NONE, ((Latex.Markup "cmt", y), i)))) || |
336 P.position (Scan.one (T.is_kind T.Command andf is_markup mark o T.val_of)) -- |
265 (improper -- markup Verbatim) |-- P.!!!! (improper |-- text --| improper_end) |
337 Scan.repeat tag -- |
266 >> (fn y => (true, (NONE, ((Latex.Verbatim, y), i)))) || |
338 P.!!!! (improper |-- P.position P.text --| improper_end) |
267 P.position (Scan.one T.not_eof) |
339 >> (fn (((tok, pos), tags), txt) => |
268 >> (fn (x, pos) => (T.is_kind T.Command x, (SOME false, ((Latex.Basic x, ("", pos)), i)))))); |
340 let val name = T.val_of tok |
269 |
341 in (SOME (name, pos, tags), (flag, mk (name, txt), d)) end)); |
270 val body = Scan.any (not o fst andf not o #2 stopper); |
342 |
271 val section = body -- Scan.one fst -- body |
343 val command = Scan.peek (fn d => |
272 >> (fn ((b1, c), b2) => (#1 (#2 c), map (snd o snd) (b1 @ (c :: b2)))); |
344 P.position (Scan.one (T.is_kind T.Command)) -- |
273 |
345 Scan.repeat tag |
274 val cmds = |
346 >> (fn ((tok, pos), tags) => |
|
347 let val name = T.val_of tok |
|
348 in (SOME (name, pos, tags), (Latex.markup_false, BasicToken tok, d)) end)); |
|
349 |
|
350 val cmt = Scan.peek (fn d => |
|
351 P.$$$ "--" |-- P.!!!! (improper |-- P.position P.text) |
|
352 >> (fn txt => (NONE, ("", MarkupToken ("cmt", txt), d)))); |
|
353 |
|
354 val other = Scan.peek (fn d => |
|
355 Scan.one T.not_eof >> (fn tok => (NONE, ("", BasicToken tok, d)))); |
|
356 |
|
357 val token = |
|
358 ignored || |
|
359 markup Latex.markup_true Markup MarkupToken || |
|
360 markup Latex.markup_true MarkupEnv MarkupEnvToken || |
|
361 markup "" Verbatim (VerbatimToken o #2) || |
|
362 command || cmt || other; |
|
363 |
|
364 |
|
365 (* spans *) |
|
366 |
|
367 val stopper = |
|
368 ((NONE, ("", BasicToken (#1 T.stopper), 0)), |
|
369 fn (_, (_, BasicToken x, _)) => #2 T.stopper x | _ => false); |
|
370 |
|
371 val cmd = Scan.one (is_some o #1); |
|
372 val non_cmd = Scan.one (is_none o #1 andf not o #2 stopper) >> #2; |
|
373 |
|
374 val comments = Scan.any (comment_token o #2 o #2); |
|
375 val blank = Scan.one (blank_token o #2 o #2); |
|
376 val newline = Scan.one (newline_token o #2 o #2); |
|
377 val before_cmd = |
|
378 Scan.option (newline -- comments) -- |
|
379 Scan.option (newline -- comments) -- |
|
380 Scan.option (blank -- comments) -- cmd; |
|
381 |
|
382 val span = |
|
383 Scan.repeat non_cmd -- cmd -- |
|
384 Scan.repeat (Scan.unless before_cmd non_cmd) -- |
|
385 Scan.option (newline >> (single o #2)) |
|
386 >> (fn (((toks1, (cmd, tok2)), toks3), tok4) => |
|
387 make_span (the cmd) (toks1 @ tok2 :: toks3 @ if_none tok4 [])); |
|
388 |
|
389 val spans = |
275 src |
390 src |
276 |> Source.filter (not o T.is_semicolon) |
391 |> Source.filter (not o T.is_semicolon) |
277 |> Source.source' 0 T.stopper (Scan.error (Scan.bulk (ignore_cmd || token))) NONE |
392 |> Source.source' 0 T.stopper (Scan.error (Scan.bulk token)) NONE |
278 |> Source.source stopper (Scan.error (Scan.bulk section)) NONE |
393 |> Source.source stopper (Scan.error (Scan.bulk span)) NONE |
279 |> Source.exhaust; |
394 |> Source.exhaust; |
280 in |
395 in |
281 if length cmds = length trs then |
396 if length trs = length spans then |
282 (trs ~~ map (present_tokens lex) cmds, Buffer.empty) |
397 ((NONE, []), NONE, true, Buffer.empty, (I, I)) |
|
398 |> Toplevel.present_excursion (trs ~~ map (present_span lex default_tags) spans) |
|
399 |> present_trailer |
283 else error "Messed-up outer syntax for presentation" |
400 else error "Messed-up outer syntax for presentation" |
284 end; |
401 end; |
285 |
402 |
286 end; |
403 end; |
287 |
404 |
356 |
449 |
357 fun pretty_term_const ctxt t = |
450 fun pretty_term_const ctxt t = |
358 if Term.is_Const t then pretty_term ctxt t |
451 if Term.is_Const t then pretty_term ctxt t |
359 else error ("Logical constant expected: " ^ ProofContext.string_of_term ctxt t); |
452 else error ("Logical constant expected: " ^ ProofContext.string_of_term ctxt t); |
360 |
453 |
361 fun pretty_thm ctxt = pretty_term ctxt o Thm.prop_of; |
454 fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of; |
362 |
455 |
363 fun pretty_term_style ctxt (name, term) = |
456 fun pretty_term_style ctxt (name, t) = |
364 let |
457 pretty_term ctxt (TermStyle.the_style (ProofContext.theory_of ctxt) name ctxt t); |
365 val thy = ProofContext.theory_of ctxt |
458 |
366 in pretty_term ctxt (TermStyle.the_style thy name ctxt term) end; |
459 fun pretty_thm_style ctxt (name, th) = |
367 |
460 pretty_term_style ctxt (name, Thm.full_prop_of th); |
368 fun pretty_thm_style ctxt (name, thm) = pretty_term_style ctxt (name, Thm.prop_of thm); |
461 |
369 |
462 fun pretty_prf full ctxt thms = |
370 fun pretty_prf full ctxt thms = (* FIXME context syntax!? *) |
463 Pretty.chunks (map (ProofContext.pretty_proof_of ctxt full) thms); |
371 Pretty.chunks (map (ProofSyntax.pretty_proof_of full) thms); |
464 |
372 |
465 |
373 fun pretty_mlidf mlidf = |
466 (* Isar output *) |
374 (use_text Context.ml_output false ("val _ = fn _ => " ^ mlidf ^ ";"); |
467 |
375 Pretty.str mlidf); |
468 fun output_list pretty src ctxt xs = |
376 |
469 map (pretty ctxt) xs (*always pretty in order to exhibit errors!*) |
377 fun output_with pretty src ctxt x = |
470 |> (if ! source then K [pretty_text (str_of_source src)] else I) |
378 let |
471 |> (if ! quotes then map Pretty.quote else I) |
379 val prt = pretty ctxt x; (*always pretty in order to catch errors!*) |
472 |> (if ! display then |
380 val prt' = if ! source then pretty_source src else prt; |
473 map (Output.output o Pretty.string_of o Pretty.indent (! indent)) |
381 in cond_display (cond_quote prt') end; |
474 #> space_implode "\\isasep\\isanewline%\n" |
382 |
475 #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" |
383 fun output_seq_with pretty src ctxt xs = |
476 else |
384 let |
477 map (Output.output o (if ! break then Pretty.string_of else Pretty.str_of)) |
385 val prts = map (pretty ctxt) xs; (*always pretty in order to catch errors!*) |
478 #> space_implode "\\isasep\\isanewline%\n" |
386 val prts' = if ! source then [pretty_source src] else prts; |
479 #> enclose "\\isa{" "}"); |
387 in cond_seq_display (map cond_quote prts') end; |
480 |
388 |
481 fun output pretty src ctxt = output_list pretty src ctxt o single; |
389 fun output_goals main_goal src state = args (Scan.succeed ()) (output_with (fn _ => fn _ => |
482 |
|
483 fun output_goals main_goal src state = args (Scan.succeed ()) (output (fn _ => fn _ => |
390 Pretty.chunks (Proof.pretty_goals main_goal (Toplevel.proof_of state |
484 Pretty.chunks (Proof.pretty_goals main_goal (Toplevel.proof_of state |
391 handle Toplevel.UNDEF => error "No proof state")))) src state; |
485 handle Toplevel.UNDEF => error "No proof state")))) src state; |
392 |
486 |
393 val _ = add_commands [ |
487 fun output_ml src ctxt txt = |
394 ("thm", args Attrib.local_thmss (output_seq_with pretty_thm)), |
488 (Context.use_mltext ("fn _ => (" ^ txt ^ ")") false (SOME (ProofContext.theory_of ctxt)); |
395 ("thm_style", args ((Scan.lift (Args.name || Args.symbol)) -- Attrib.local_thm) (output_with pretty_thm_style)), |
489 (if ! source then str_of_source src else txt) |
396 ("prop", args Args.local_prop (output_with pretty_term)), |
490 |> (if ! quotes then quote else I) |
397 ("term", args Args.local_term (output_with pretty_term)), |
491 |> (if ! display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}" |
398 ("term_style", args ((Scan.lift (Args.name || Args.symbol)) -- Args.local_term) (output_with pretty_term_style)), |
492 else |
399 ("term_type", args Args.local_term (output_with pretty_term_typ)), |
493 split_lines |
400 ("typeof", args Args.local_term (output_with pretty_term_typeof)), |
494 #> map (space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|") |
401 ("const", args Args.local_term (output_with pretty_term_const)), |
495 #> space_implode "\\isasep\\isanewline%\n")); |
402 ("typ", args Args.local_typ_abbrev (output_with ProofContext.pretty_typ)), |
496 |
403 ("text", args (Scan.lift Args.name) (output_with (K pretty_text))), |
497 |
|
498 (* commands *) |
|
499 |
|
500 val _ = add_commands |
|
501 [("thm", args Attrib.local_thmss (output_list pretty_thm)), |
|
502 ("thm_style", args (Scan.lift Args.liberal_name -- Attrib.local_thm) (output pretty_thm_style)), |
|
503 ("prop", args Args.local_prop (output pretty_term)), |
|
504 ("term", args Args.local_term (output pretty_term)), |
|
505 ("term_style", args (Scan.lift Args.liberal_name -- Args.local_term) (output pretty_term_style)), |
|
506 ("term_type", args Args.local_term (output pretty_term_typ)), |
|
507 ("typeof", args Args.local_term (output pretty_term_typeof)), |
|
508 ("const", args Args.local_term (output pretty_term_const)), |
|
509 ("typ", args Args.local_typ_abbrev (output ProofContext.pretty_typ)), |
|
510 ("text", args (Scan.lift Args.name) (output (K pretty_text))), |
404 ("goals", output_goals true), |
511 ("goals", output_goals true), |
405 ("subgoals", output_goals false), |
512 ("subgoals", output_goals false), |
406 ("prf", args Attrib.local_thmss (output_with (pretty_prf false))), |
513 ("prf", args Attrib.local_thmss (output (pretty_prf false))), |
407 ("full_prf", args Attrib.local_thmss (output_with (pretty_prf true))), |
514 ("full_prf", args Attrib.local_thmss (output (pretty_prf true))), |
408 (*this is just experimental*) |
515 ("ML", args (Scan.lift Args.name) output_ml)]; |
409 ("ML_idf", args (Scan.lift (Args.name || Args.symbol)) (output_with (K pretty_mlidf))) |
|
410 ]; |
|
411 |
516 |
412 end; |
517 end; |