133 val property = P.xname -- Scan.optional (P.$$$ "=" |-- P.!!! P.xname) ""; |
133 val property = P.xname -- Scan.optional (P.$$$ "=" |-- P.!!! P.xname) ""; |
134 val properties = Scan.optional (P.$$$ "[" |-- P.!!! (P.enum "," property --| P.$$$ "]")) []; |
134 val properties = Scan.optional (P.$$$ "[" |-- P.!!! (P.enum "," property --| P.$$$ "]")) []; |
135 |
135 |
136 in |
136 in |
137 |
137 |
138 val antiq = P.!!! (P.position P.xname -- properties -- P.arguments --| Scan.ahead P.eof) |
138 val antiq = P.!!! (P.position P.xname -- properties -- Args.parse --| Scan.ahead P.eof) |
139 >> (fn (((x, pos), y), z) => (y, Args.src ((x, z), pos))); |
139 >> (fn (((x, pos), y), z) => (y, Args.src ((x, z), pos))); |
140 |
140 |
141 end; |
141 end; |
142 |
142 |
143 |
143 |
330 |
330 |
331 val ignored = Scan.state --| ignore |
331 val ignored = Scan.state --| ignore |
332 >> (fn d => (NONE, (NoToken, ("", d)))); |
332 >> (fn d => (NONE, (NoToken, ("", d)))); |
333 |
333 |
334 fun markup mark mk flag = Scan.peek (fn d => |
334 fun markup mark mk flag = Scan.peek (fn d => |
335 improper |-- P.position (Scan.one (T.is_kind T.Command andf is_markup mark o T.val_of)) -- |
335 improper |-- P.position (Scan.one (T.is_kind T.Command andf is_markup mark o T.content_of)) -- |
336 Scan.repeat tag -- |
336 Scan.repeat tag -- |
337 P.!!!! ((improper -- locale -- improper) |-- P.position P.text --| improper_end) |
337 P.!!!! ((improper -- locale -- improper) |-- P.position P.text --| improper_end) |
338 >> (fn (((tok, pos), tags), txt) => |
338 >> (fn (((tok, pos), tags), txt) => |
339 let val name = T.val_of tok |
339 let val name = T.content_of tok |
340 in (SOME (name, pos, tags), (mk (name, txt), (flag, d))) end)); |
340 in (SOME (name, pos, tags), (mk (name, txt), (flag, d))) end)); |
341 |
341 |
342 val command = Scan.peek (fn d => |
342 val command = Scan.peek (fn d => |
343 P.position (Scan.one (T.is_kind T.Command)) -- |
343 P.position (Scan.one (T.is_kind T.Command)) -- |
344 Scan.repeat tag |
344 Scan.repeat tag |
345 >> (fn ((tok, pos), tags) => |
345 >> (fn ((tok, pos), tags) => |
346 let val name = T.val_of tok |
346 let val name = T.content_of tok |
347 in (SOME (name, pos, tags), (BasicToken tok, (Latex.markup_false, d))) end)); |
347 in (SOME (name, pos, tags), (BasicToken tok, (Latex.markup_false, d))) end)); |
348 |
348 |
349 val cmt = Scan.peek (fn d => |
349 val cmt = Scan.peek (fn d => |
350 P.$$$ "--" |-- P.!!!! (improper |-- P.position P.text) |
350 P.$$$ "--" |-- P.!!!! (improper |-- P.position P.text) |
351 >> (fn txt => (NONE, (MarkupToken ("cmt", txt), ("", d))))); |
351 >> (fn txt => (NONE, (MarkupToken ("cmt", txt), ("", d))))); |
426 ("goals_limit", Library.setmp goals_limit o integer)]; |
426 ("goals_limit", Library.setmp goals_limit o integer)]; |
427 |
427 |
428 |
428 |
429 (* basic pretty printing *) |
429 (* basic pretty printing *) |
430 |
430 |
431 val str_of_source = space_implode " " o map Args.string_of o #2 o #1 o Args.dest_src; |
431 val str_of_source = space_implode " " o map T.unparse o #2 o #1 o Args.dest_src; |
432 |
432 |
433 fun tweak_line s = |
433 fun tweak_line s = |
434 if ! display then s else Symbol.strip_blanks s; |
434 if ! display then s else Symbol.strip_blanks s; |
435 |
435 |
436 val pretty_text = Pretty.chunks o map Pretty.str o map tweak_line o Library.split_lines; |
436 val pretty_text = Pretty.chunks o map Pretty.str o map tweak_line o Library.split_lines; |
525 |> Proof.theorem_i NONE (K I) [[(prop, [])]] |
525 |> Proof.theorem_i NONE (K I) [[(prop, [])]] |
526 |> Proof.global_terminal_proof methods; |
526 |> Proof.global_terminal_proof methods; |
527 in pretty_term ctxt prop end; |
527 in pretty_term ctxt prop end; |
528 |
528 |
529 val embedded_lemma = |
529 val embedded_lemma = |
530 args (Args.prop -- Scan.lift (Args.$$$ "by" |-- Method.parse_args -- Scan.option Method.parse_args)) |
530 args (Args.prop -- Scan.lift (Args.$$$ "by" |-- Method.parse -- Scan.option Method.parse)) |
531 (output pretty_lemma o (fn ((a, arg :: _), p) => (Args.src ((a, [arg]), p))) o Args.dest_src); |
531 (output pretty_lemma o (fn ((a, arg :: _), p) => (Args.src ((a, [arg]), p))) o Args.dest_src); |
532 |
532 |
533 |
533 |
534 (* commands *) |
534 (* commands *) |
535 |
535 |
551 ("goals", output_goals true), |
551 ("goals", output_goals true), |
552 ("subgoals", output_goals false), |
552 ("subgoals", output_goals false), |
553 ("prf", args Attrib.thms (output (pretty_prf false))), |
553 ("prf", args Attrib.thms (output (pretty_prf false))), |
554 ("full_prf", args Attrib.thms (output (pretty_prf true))), |
554 ("full_prf", args Attrib.thms (output (pretty_prf true))), |
555 ("theory", args (Scan.lift Args.name) (output pretty_theory)), |
555 ("theory", args (Scan.lift Args.name) (output pretty_theory)), |
556 ("ML", args (Scan.lift (Args.position Args.name)) (output_ml ml_val)), |
556 ("ML", args (Scan.lift (P.position Args.name)) (output_ml ml_val)), |
557 ("ML_type", args (Scan.lift (Args.position Args.name)) (output_ml ml_type)), |
557 ("ML_type", args (Scan.lift (P.position Args.name)) (output_ml ml_type)), |
558 ("ML_struct", args (Scan.lift (Args.position Args.name)) (output_ml ml_struct))]; |
558 ("ML_struct", args (Scan.lift (P.position Args.name)) (output_ml ml_struct))]; |
559 |
559 |
560 end; |
560 end; |