1.1 --- a/src/Pure/Isar/isar_output.ML Fri Jan 19 22:08:32 2007 +0100
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,545 +0,0 @@
1.4 -(* Title: Pure/Isar/isar_output.ML
1.5 - ID: $Id$
1.6 - Author: Markus Wenzel, TU Muenchen
1.7 -
1.8 -Isar theory output.
1.9 -*)
1.10 -
1.11 -signature ISAR_OUTPUT =
1.12 -sig
1.13 - val display: bool ref
1.14 - val quotes: bool ref
1.15 - val indent: int ref
1.16 - val source: bool ref
1.17 - val add_commands: (string * (Args.src -> Toplevel.node option -> string)) list -> unit
1.18 - val add_options: (string * (string -> (unit -> string) -> unit -> string)) list -> unit
1.19 - val print_antiquotations: unit -> unit
1.20 - val boolean: string -> bool
1.21 - val integer: string -> int
1.22 - val args: (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list)) ->
1.23 - (Args.src -> Proof.context -> 'a -> string) -> Args.src -> Toplevel.node option -> string
1.24 - datatype markup = Markup | MarkupEnv | Verbatim
1.25 - val modes: string list ref
1.26 - val eval_antiquote: Scan.lexicon -> Toplevel.node option -> string * Position.T -> string
1.27 - val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
1.28 - Toplevel.transition list -> (OuterLex.token, 'a) Source.source -> Buffer.T
1.29 - val output_list: (Proof.context -> 'a -> Pretty.T) -> Args.src ->
1.30 - Proof.context -> 'a list -> string
1.31 - val output: (Proof.context -> 'a -> Pretty.T) -> Args.src -> Proof.context -> 'a -> string
1.32 -end;
1.33 -
1.34 -structure IsarOutput: ISAR_OUTPUT =
1.35 -struct
1.36 -
1.37 -structure T = OuterLex;
1.38 -structure P = OuterParse;
1.39 -
1.40 -
1.41 -(** global options **)
1.42 -
1.43 -val locale = ref "";
1.44 -val display = ref false;
1.45 -val quotes = ref false;
1.46 -val indent = ref 0;
1.47 -val source = ref false;
1.48 -val break = ref false;
1.49 -
1.50 -
1.51 -
1.52 -(** maintain global commands **)
1.53 -
1.54 -local
1.55 -
1.56 -val global_commands =
1.57 - ref (Symtab.empty: (Args.src -> Toplevel.node option -> string) Symtab.table);
1.58 -
1.59 -val global_options =
1.60 - ref (Symtab.empty: (string -> (unit -> string) -> unit -> string) Symtab.table);
1.61 -
1.62 -fun add_item kind (name, x) tab =
1.63 - (if not (Symtab.defined tab name) then ()
1.64 - else warning ("Redefined antiquotation " ^ kind ^ ": " ^ quote name);
1.65 - Symtab.update (name, x) tab);
1.66 -
1.67 -in
1.68 -
1.69 -val add_commands = Library.change global_commands o fold (add_item "command");
1.70 -val add_options = Library.change global_options o fold (add_item "option");
1.71 -
1.72 -fun command src =
1.73 - let val ((name, _), pos) = Args.dest_src src in
1.74 - (case Symtab.lookup (! global_commands) name of
1.75 - NONE => error ("Unknown antiquotation command: " ^ quote name ^ Position.str_of pos)
1.76 - | SOME f => transform_failure (curry Antiquote.ANTIQUOTE_FAIL (name, pos)) (f src))
1.77 - end;
1.78 -
1.79 -fun option (name, s) f () =
1.80 - (case Symtab.lookup (! global_options) name of
1.81 - NONE => error ("Unknown antiquotation option: " ^ quote name)
1.82 - | SOME opt => opt s f ());
1.83 -
1.84 -fun options [] f = f
1.85 - | options (opt :: opts) f = option opt (options opts f);
1.86 -
1.87 -
1.88 -fun print_antiquotations () =
1.89 - [Pretty.big_list "antiquotation commands:" (map Pretty.str (Symtab.keys (! global_commands))),
1.90 - Pretty.big_list "antiquotation options:" (map Pretty.str (Symtab.keys (! global_options)))]
1.91 - |> Pretty.chunks |> Pretty.writeln;
1.92 -
1.93 -end;
1.94 -
1.95 -
1.96 -
1.97 -(** syntax of antiquotations **)
1.98 -
1.99 -(* option values *)
1.100 -
1.101 -fun boolean "" = true
1.102 - | boolean "true" = true
1.103 - | boolean "false" = false
1.104 - | boolean s = error ("Bad boolean value: " ^ quote s);
1.105 -
1.106 -fun integer s =
1.107 - let
1.108 - fun int ss =
1.109 - (case Library.read_int ss of (i, []) => i
1.110 - | _ => error ("Bad integer value: " ^ quote s));
1.111 - in (case Symbol.explode s of "-" :: ss => ~ (int ss) | ss => int ss) end;
1.112 -
1.113 -
1.114 -(* args syntax *)
1.115 -
1.116 -fun syntax scan = Args.context_syntax "antiquotation" scan;
1.117 -
1.118 -fun args scan f src node : string =
1.119 - let
1.120 - val loc = if ! locale = "" then NONE else SOME (! locale);
1.121 - val (x, ctxt) = syntax scan src (Toplevel.presentation_context node loc);
1.122 - in f src ctxt x end;
1.123 -
1.124 -
1.125 -(* outer syntax *)
1.126 -
1.127 -local
1.128 -
1.129 -val property = P.xname -- Scan.optional (P.$$$ "=" |-- P.!!! P.xname) "";
1.130 -val properties = Scan.optional (P.$$$ "[" |-- P.!!! (P.enum "," property --| P.$$$ "]")) [];
1.131 -
1.132 -val antiq = P.position P.xname -- properties -- P.arguments --| Scan.ahead P.eof
1.133 - >> (fn (((x, pos), y), z) => (y, Args.src ((x, z), pos)));
1.134 -
1.135 -fun antiq_args_aux keyword_lexicon (str, pos) =
1.136 - Source.of_string str
1.137 - |> Symbol.source false
1.138 - |> T.source false (K (keyword_lexicon, Scan.empty_lexicon)) pos
1.139 - |> T.source_proper
1.140 - |> Source.source T.stopper (Scan.error (Scan.bulk (P.!!! antiq))) NONE
1.141 - |> Source.exhaust;
1.142 -
1.143 -in
1.144 -
1.145 -fun antiq_args lex (s, pos) =
1.146 - let
1.147 - fun err msg = cat_error msg
1.148 - ("Malformed antiquotation: " ^ quote ("@{" ^ s ^ "}") ^ Position.str_of pos);
1.149 - in (case antiq_args_aux lex (s, pos) of [x] => x | _ => err "") handle ERROR msg => err msg end;
1.150 -
1.151 -end;
1.152 -
1.153 -
1.154 -(* eval_antiquote *)
1.155 -
1.156 -val modes = ref ([]: string list);
1.157 -
1.158 -fun eval_antiquote lex node (str, pos) =
1.159 - let
1.160 - fun expand (Antiquote.Text s) = s
1.161 - | expand (Antiquote.Antiq x) =
1.162 - let val (opts, src) = antiq_args lex x in
1.163 - options opts (fn () => command src node) (); (*preview errors!*)
1.164 - Library.setmp print_mode (! modes @ Latex.modes @ ! print_mode)
1.165 - (Output.no_warnings (options opts (fn () => command src node))) ()
1.166 - end;
1.167 - val ants = Antiquote.antiquotes_of (str, pos);
1.168 - in
1.169 - if is_none node andalso exists Antiquote.is_antiq ants then
1.170 - error ("Cannot expand antiquotations at top-level" ^ Position.str_of pos)
1.171 - else implode (map expand ants)
1.172 - end;
1.173 -
1.174 -
1.175 -
1.176 -(** present theory source **)
1.177 -
1.178 -(*NB: arranging white space around command spans is a black art.*)
1.179 -
1.180 -(* presentation tokens *)
1.181 -
1.182 -datatype token =
1.183 - NoToken
1.184 - | BasicToken of T.token
1.185 - | MarkupToken of string * (string * Position.T)
1.186 - | MarkupEnvToken of string * (string * Position.T)
1.187 - | VerbatimToken of string * Position.T;
1.188 -
1.189 -fun output_token lex state =
1.190 - let
1.191 - val eval = eval_antiquote lex (try Toplevel.node_of state)
1.192 - in
1.193 - fn NoToken => ""
1.194 - | BasicToken tok => Latex.output_basic tok
1.195 - | MarkupToken (cmd, txt) => Latex.output_markup cmd (eval txt)
1.196 - | MarkupEnvToken (cmd, txt) => Latex.output_markup_env cmd (eval txt)
1.197 - | VerbatimToken txt => Latex.output_verbatim (eval txt)
1.198 - end;
1.199 -
1.200 -fun basic_token pred (BasicToken tok) = pred tok
1.201 - | basic_token _ _ = false;
1.202 -
1.203 -val improper_token = basic_token (not o T.is_proper);
1.204 -val comment_token = basic_token T.is_comment;
1.205 -val blank_token = basic_token T.is_blank;
1.206 -val newline_token = basic_token T.is_newline;
1.207 -
1.208 -
1.209 -(* command spans *)
1.210 -
1.211 -type command = string * Position.T * string list; (*name, position, tags*)
1.212 -type source = (token * (string * int)) list; (*token, markup flag, meta-comment depth*)
1.213 -
1.214 -datatype span = Span of command * (source * source * source * source) * bool;
1.215 -
1.216 -fun make_span cmd src =
1.217 - let
1.218 - fun take_newline (tok :: toks) =
1.219 - if newline_token (fst tok) then ([tok], toks, true)
1.220 - else ([], tok :: toks, false)
1.221 - | take_newline [] = ([], [], false);
1.222 - val (((src_prefix, src_main), src_suffix1), (src_suffix2, src_appendix, newline)) =
1.223 - src
1.224 - |> take_prefix (improper_token o fst)
1.225 - ||>> take_suffix (improper_token o fst)
1.226 - ||>> take_prefix (comment_token o fst)
1.227 - ||> take_newline;
1.228 - in Span (cmd, (src_prefix, src_main, src_suffix1 @ src_suffix2, src_appendix), newline) end;
1.229 -
1.230 -
1.231 -(* present spans *)
1.232 -
1.233 -local
1.234 -
1.235 -fun err_bad_nesting pos =
1.236 - error ("Bad nesting of commands in presentation" ^ pos);
1.237 -
1.238 -fun edge which f (x: string option, y) =
1.239 - if x = y then I
1.240 - else (case which (x, y) of NONE => I | SOME txt => Buffer.add (f txt));
1.241 -
1.242 -val begin_tag = edge #2 Latex.begin_tag;
1.243 -val end_tag = edge #1 Latex.end_tag;
1.244 -fun open_delim delim e = edge #2 Latex.begin_delim e #> delim #> edge #2 Latex.end_delim e;
1.245 -fun close_delim delim e = edge #1 Latex.begin_delim e #> delim #> edge #1 Latex.end_delim e;
1.246 -
1.247 -in
1.248 -
1.249 -fun present_span lex default_tags span state state'
1.250 - (tag_stack, active_tag, newline, buffer, present_cont) =
1.251 - let
1.252 - val present = fold (fn (tok, (flag, 0)) =>
1.253 - Buffer.add (output_token lex state' tok)
1.254 - #> Buffer.add flag
1.255 - | _ => I);
1.256 -
1.257 - val Span ((cmd_name, cmd_pos, cmd_tags), srcs, span_newline) = span;
1.258 -
1.259 - val (tag, tags) = tag_stack;
1.260 - val tag' = try hd (fold OuterKeyword.update_tags cmd_tags (the_list tag));
1.261 -
1.262 - val active_tag' =
1.263 - if is_some tag' then tag'
1.264 - else if cmd_name = "end" andalso not (Toplevel.is_toplevel state') then NONE
1.265 - else try hd (default_tags cmd_name);
1.266 - val edge = (active_tag, active_tag');
1.267 -
1.268 - val newline' =
1.269 - if is_none active_tag' then span_newline else newline;
1.270 -
1.271 - val nesting = Toplevel.level state' - Toplevel.level state;
1.272 - val tag_stack' =
1.273 - if nesting = 0 andalso not (Toplevel.is_proof state) then tag_stack
1.274 - else if nesting >= 0 then (tag', replicate nesting tag @ tags)
1.275 - else
1.276 - (case Library.drop (~ nesting - 1, tags) of
1.277 - tgs :: tgss => (tgs, tgss)
1.278 - | [] => err_bad_nesting (Position.str_of cmd_pos));
1.279 -
1.280 - val buffer' =
1.281 - buffer
1.282 - |> end_tag edge
1.283 - |> close_delim (fst present_cont) edge
1.284 - |> snd present_cont
1.285 - |> open_delim (present (#1 srcs)) edge
1.286 - |> begin_tag edge
1.287 - |> present (#2 srcs);
1.288 - val present_cont' =
1.289 - if newline then (present (#3 srcs), present (#4 srcs))
1.290 - else (I, present (#3 srcs) #> present (#4 srcs));
1.291 - in (tag_stack', active_tag', newline', buffer', present_cont') end;
1.292 -
1.293 -fun present_trailer ((_, tags), active_tag, _, buffer, present_cont) =
1.294 - if not (null tags) then err_bad_nesting " at end of theory"
1.295 - else
1.296 - buffer
1.297 - |> end_tag (active_tag, NONE)
1.298 - |> close_delim (fst present_cont) (active_tag, NONE)
1.299 - |> snd present_cont;
1.300 -
1.301 -end;
1.302 -
1.303 -
1.304 -(* present_thy *)
1.305 -
1.306 -datatype markup = Markup | MarkupEnv | Verbatim;
1.307 -
1.308 -local
1.309 -
1.310 -val space_proper =
1.311 - Scan.one T.is_blank -- Scan.many T.is_comment -- Scan.one T.is_proper;
1.312 -
1.313 -val is_improper = not o (T.is_proper orf T.is_begin_ignore orf T.is_end_ignore);
1.314 -val improper = Scan.many is_improper;
1.315 -val improper_end = Scan.repeat (Scan.unless space_proper (Scan.one is_improper));
1.316 -val blank_end = Scan.repeat (Scan.unless space_proper (Scan.one T.is_blank));
1.317 -
1.318 -val opt_newline = Scan.option (Scan.one T.is_newline);
1.319 -
1.320 -val ignore =
1.321 - Scan.depend (fn d => opt_newline |-- Scan.one T.is_begin_ignore
1.322 - >> pair (d + 1)) ||
1.323 - Scan.depend (fn d => Scan.one T.is_end_ignore --|
1.324 - (if d = 0 then Scan.fail_with (K "Bad nesting of meta-comments") else opt_newline)
1.325 - >> pair (d - 1));
1.326 -
1.327 -val tag = (improper -- P.$$$ "%" -- improper) |-- P.!!! (P.tag_name --| blank_end);
1.328 -
1.329 -val locale =
1.330 - Scan.option ((P.$$$ "(" -- improper -- P.$$$ "in") |--
1.331 - P.!!! (improper |-- P.xname --| (improper -- P.$$$ ")")));
1.332 -
1.333 -in
1.334 -
1.335 -fun present_thy lex default_tags is_markup trs src =
1.336 - let
1.337 - (* tokens *)
1.338 -
1.339 - val ignored = Scan.state --| ignore
1.340 - >> (fn d => (NONE, (NoToken, ("", d))));
1.341 -
1.342 - fun markup mark mk flag = Scan.peek (fn d =>
1.343 - improper |-- P.position (Scan.one (T.is_kind T.Command andf is_markup mark o T.val_of)) --
1.344 - Scan.repeat tag --
1.345 - P.!!!! ((improper -- locale -- improper) |-- P.position P.text --| improper_end)
1.346 - >> (fn (((tok, pos), tags), txt) =>
1.347 - let val name = T.val_of tok
1.348 - in (SOME (name, pos, tags), (mk (name, txt), (flag, d))) end));
1.349 -
1.350 - val command = Scan.peek (fn d =>
1.351 - P.position (Scan.one (T.is_kind T.Command)) --
1.352 - Scan.repeat tag
1.353 - >> (fn ((tok, pos), tags) =>
1.354 - let val name = T.val_of tok
1.355 - in (SOME (name, pos, tags), (BasicToken tok, (Latex.markup_false, d))) end));
1.356 -
1.357 - val cmt = Scan.peek (fn d =>
1.358 - P.$$$ "--" |-- P.!!!! (improper |-- P.position P.text)
1.359 - >> (fn txt => (NONE, (MarkupToken ("cmt", txt), ("", d)))));
1.360 -
1.361 - val other = Scan.peek (fn d =>
1.362 - Scan.one T.not_eof >> (fn tok => (NONE, (BasicToken tok, ("", d)))));
1.363 -
1.364 - val token =
1.365 - ignored ||
1.366 - markup Markup MarkupToken Latex.markup_true ||
1.367 - markup MarkupEnv MarkupEnvToken Latex.markup_true ||
1.368 - markup Verbatim (VerbatimToken o #2) "" ||
1.369 - command || cmt || other;
1.370 -
1.371 -
1.372 - (* spans *)
1.373 -
1.374 - val stopper =
1.375 - ((NONE, (BasicToken (#1 T.stopper), ("", 0))),
1.376 - fn (_, (BasicToken x, _)) => #2 T.stopper x | _ => false);
1.377 -
1.378 - val cmd = Scan.one (is_some o fst);
1.379 - val non_cmd = Scan.one (is_none o fst andf not o #2 stopper) >> #2;
1.380 -
1.381 - val comments = Scan.many (comment_token o fst o snd);
1.382 - val blank = Scan.one (blank_token o fst o snd);
1.383 - val newline = Scan.one (newline_token o fst o snd);
1.384 - val before_cmd =
1.385 - Scan.option (newline -- comments) --
1.386 - Scan.option (newline -- comments) --
1.387 - Scan.option (blank -- comments) -- cmd;
1.388 -
1.389 - val span =
1.390 - Scan.repeat non_cmd -- cmd --
1.391 - Scan.repeat (Scan.unless before_cmd non_cmd) --
1.392 - Scan.option (newline >> (single o snd))
1.393 - >> (fn (((toks1, (cmd, tok2)), toks3), tok4) =>
1.394 - make_span (the cmd) (toks1 @ (tok2 :: (toks3 @ the_default [] tok4))));
1.395 -
1.396 - val spans =
1.397 - src
1.398 - |> Source.filter (not o T.is_semicolon)
1.399 - |> Source.source' 0 T.stopper (Scan.error (Scan.bulk token)) NONE
1.400 - |> Source.source stopper (Scan.error (Scan.bulk span)) NONE
1.401 - |> Source.exhaust;
1.402 - in
1.403 - if length trs = length spans then
1.404 - ((NONE, []), NONE, true, Buffer.empty, (I, I))
1.405 - |> Toplevel.present_excursion (trs ~~ map (present_span lex default_tags) spans)
1.406 - |> present_trailer
1.407 - else error "Messed-up outer syntax for presentation"
1.408 - end;
1.409 -
1.410 -end;
1.411 -
1.412 -
1.413 -
1.414 -(** setup default output **)
1.415 -
1.416 -(* options *)
1.417 -
1.418 -val _ = add_options
1.419 - [("show_types", Library.setmp Syntax.show_types o boolean),
1.420 - ("show_sorts", Library.setmp Syntax.show_sorts o boolean),
1.421 - ("show_structs", Library.setmp show_structs o boolean),
1.422 - ("show_question_marks", Library.setmp show_question_marks o boolean),
1.423 - ("long_names", Library.setmp NameSpace.long_names o boolean),
1.424 - ("short_names", Library.setmp NameSpace.short_names o boolean),
1.425 - ("unique_names", Library.setmp NameSpace.unique_names o boolean),
1.426 - ("eta_contract", Library.setmp Syntax.eta_contract o boolean),
1.427 - ("locale", Library.setmp locale),
1.428 - ("display", Library.setmp display o boolean),
1.429 - ("break", Library.setmp break o boolean),
1.430 - ("quotes", Library.setmp quotes o boolean),
1.431 - ("mode", fn s => fn f => fn () => Library.setmp print_mode (s :: ! print_mode) f ()),
1.432 - ("margin", Pretty.setmp_margin o integer),
1.433 - ("indent", Library.setmp indent o integer),
1.434 - ("source", Library.setmp source o boolean),
1.435 - ("goals_limit", Library.setmp goals_limit o integer)];
1.436 -
1.437 -
1.438 -(* basic pretty printing *)
1.439 -
1.440 -val str_of_source = space_implode " " o map Args.string_of o #2 o #1 o Args.dest_src;
1.441 -
1.442 -fun tweak_line s =
1.443 - if ! display then s else Symbol.strip_blanks s;
1.444 -
1.445 -val pretty_text = Pretty.chunks o map Pretty.str o map tweak_line o Library.split_lines;
1.446 -
1.447 -fun pretty_term ctxt = ProofContext.pretty_term ctxt o ProofContext.revert_skolems ctxt;
1.448 -fun pretty_term_abbrev ctxt =
1.449 - ProofContext.pretty_term_abbrev ctxt o ProofContext.revert_skolems ctxt;
1.450 -
1.451 -fun pretty_term_typ ctxt t =
1.452 - ProofContext.pretty_term ctxt (TypeInfer.constrain t (Term.fastype_of t));
1.453 -
1.454 -fun pretty_term_typeof ctxt = ProofContext.pretty_typ ctxt o Term.fastype_of;
1.455 -
1.456 -fun pretty_term_const ctxt t =
1.457 - if Term.is_Const t then pretty_term ctxt t
1.458 - else error ("Logical constant expected: " ^ ProofContext.string_of_term ctxt t);
1.459 -
1.460 -fun pretty_abbrev ctxt t =
1.461 - let
1.462 - fun err () = error ("Abbreviated constant expected: " ^ ProofContext.string_of_term ctxt t);
1.463 - val (head, args) = Term.strip_comb t;
1.464 - val (c, T) = Term.dest_Const head handle TERM _ => err ();
1.465 - val (U, (u, _)) = Consts.the_abbreviation (ProofContext.consts_of ctxt) c
1.466 - handle TYPE _ => err ();
1.467 - val t' = Term.betapplys (Envir.expand_atom T (U, u), args);
1.468 - in pretty_term_abbrev ctxt (Logic.mk_equals (t, t')) end;
1.469 -
1.470 -fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
1.471 -
1.472 -fun pretty_term_style ctxt (name, t) =
1.473 - pretty_term ctxt (TermStyle.the_style (ProofContext.theory_of ctxt) name ctxt t);
1.474 -
1.475 -fun pretty_thm_style ctxt (name, th) =
1.476 - pretty_term_style ctxt (name, Thm.full_prop_of th);
1.477 -
1.478 -fun pretty_prf full ctxt thms =
1.479 - Pretty.chunks (map (ProofContext.pretty_proof_of ctxt full) thms);
1.480 -
1.481 -fun pretty_theory ctxt name =
1.482 - (Theory.requires (ProofContext.theory_of ctxt) name "presentation"; Pretty.str name);
1.483 -
1.484 -
1.485 -(* Isar output *)
1.486 -
1.487 -fun output_list pretty src ctxt xs =
1.488 - map (pretty ctxt) xs (*always pretty in order to exhibit errors!*)
1.489 - |> (if ! source then K [pretty_text (str_of_source src)] else I)
1.490 - |> (if ! quotes then map Pretty.quote else I)
1.491 - |> (if ! display then
1.492 - map (Output.output o Pretty.string_of o Pretty.indent (! indent))
1.493 - #> space_implode "\\isasep\\isanewline%\n"
1.494 - #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
1.495 - else
1.496 - map (Output.output o (if ! break then Pretty.string_of else Pretty.str_of))
1.497 - #> space_implode "\\isasep\\isanewline%\n"
1.498 - #> enclose "\\isa{" "}");
1.499 -
1.500 -fun output pretty src ctxt = output_list pretty src ctxt o single;
1.501 -
1.502 -fun proof_state node =
1.503 - (case Option.map Toplevel.proof_node node of
1.504 - SOME (SOME prf) => ProofHistory.current prf
1.505 - | _ => error "No proof state");
1.506 -
1.507 -fun output_goals main_goal src node = args (Scan.succeed ()) (output (fn _ => fn _ =>
1.508 - Pretty.chunks (Proof.pretty_goals main_goal (proof_state node)))) src node;
1.509 -
1.510 -fun ml_val txt = "fn _ => (" ^ txt ^ ");";
1.511 -fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option;";
1.512 -fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;"
1.513 -
1.514 -fun output_ml ml src ctxt txt =
1.515 - (Context.use_mltext (ml txt) false (SOME (Context.Proof ctxt));
1.516 - (if ! source then str_of_source src else txt)
1.517 - |> (if ! quotes then quote else I)
1.518 - |> (if ! display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
1.519 - else
1.520 - split_lines
1.521 - #> map (space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|")
1.522 - #> space_implode "\\isasep\\isanewline%\n"));
1.523 -
1.524 -
1.525 -(* commands *)
1.526 -
1.527 -val _ = add_commands
1.528 - [("thm", args Attrib.thms (output_list pretty_thm)),
1.529 - ("thm_style", args (Scan.lift Args.liberal_name -- Attrib.thm) (output pretty_thm_style)),
1.530 - ("prop", args Args.prop (output pretty_term)),
1.531 - ("term", args Args.term (output pretty_term)),
1.532 - ("term_style", args (Scan.lift Args.liberal_name -- Args.term) (output pretty_term_style)),
1.533 - ("term_type", args Args.term (output pretty_term_typ)),
1.534 - ("typeof", args Args.term (output pretty_term_typeof)),
1.535 - ("const", args Args.term (output pretty_term_const)),
1.536 - ("abbrev", args Args.term_abbrev (output pretty_abbrev)),
1.537 - ("typ", args Args.typ_abbrev (output ProofContext.pretty_typ)),
1.538 - ("text", args (Scan.lift Args.name) (output (K pretty_text))),
1.539 - ("goals", output_goals true),
1.540 - ("subgoals", output_goals false),
1.541 - ("prf", args Attrib.thms (output (pretty_prf false))),
1.542 - ("full_prf", args Attrib.thms (output (pretty_prf true))),
1.543 - ("theory", args (Scan.lift Args.name) (output pretty_theory)),
1.544 - ("ML", args (Scan.lift Args.name) (output_ml ml_val)),
1.545 - ("ML_type", args (Scan.lift Args.name) (output_ml ml_type)),
1.546 - ("ML_struct", args (Scan.lift Args.name) (output_ml ml_struct))];
1.547 -
1.548 -end;
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/Pure/Thy/thy_output.ML Fri Jan 19 22:10:35 2007 +0100
2.3 @@ -0,0 +1,532 @@
2.4 +(* Title: Pure/Thy/thy_output.ML
2.5 + ID: $Id$
2.6 + Author: Markus Wenzel, TU Muenchen
2.7 +
2.8 +Theory document output.
2.9 +*)
2.10 +
2.11 +signature THY_OUTPUT =
2.12 +sig
2.13 + val display: bool ref
2.14 + val quotes: bool ref
2.15 + val indent: int ref
2.16 + val source: bool ref
2.17 + val add_commands: (string * (Args.src -> Toplevel.node option -> string)) list -> unit
2.18 + val add_options: (string * (string -> (unit -> string) -> unit -> string)) list -> unit
2.19 + val print_antiquotations: unit -> unit
2.20 + val boolean: string -> bool
2.21 + val integer: string -> int
2.22 + val args: (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list)) ->
2.23 + (Args.src -> Proof.context -> 'a -> string) -> Args.src -> Toplevel.node option -> string
2.24 + datatype markup = Markup | MarkupEnv | Verbatim
2.25 + val modes: string list ref
2.26 + val eval_antiquote: Scan.lexicon -> Toplevel.node option -> string * Position.T -> string
2.27 + val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
2.28 + Toplevel.transition list -> (OuterLex.token, 'a) Source.source -> Buffer.T
2.29 + val output_list: (Proof.context -> 'a -> Pretty.T) -> Args.src ->
2.30 + Proof.context -> 'a list -> string
2.31 + val output: (Proof.context -> 'a -> Pretty.T) -> Args.src -> Proof.context -> 'a -> string
2.32 +end;
2.33 +
2.34 +structure ThyOutput: THY_OUTPUT =
2.35 +struct
2.36 +
2.37 +structure T = OuterLex;
2.38 +structure P = OuterParse;
2.39 +
2.40 +
2.41 +(** global options **)
2.42 +
2.43 +val locale = ref "";
2.44 +val display = ref false;
2.45 +val quotes = ref false;
2.46 +val indent = ref 0;
2.47 +val source = ref false;
2.48 +val break = ref false;
2.49 +
2.50 +
2.51 +
2.52 +(** maintain global commands **)
2.53 +
2.54 +local
2.55 +
2.56 +val global_commands =
2.57 + ref (Symtab.empty: (Args.src -> Toplevel.node option -> string) Symtab.table);
2.58 +
2.59 +val global_options =
2.60 + ref (Symtab.empty: (string -> (unit -> string) -> unit -> string) Symtab.table);
2.61 +
2.62 +fun add_item kind (name, x) tab =
2.63 + (if not (Symtab.defined tab name) then ()
2.64 + else warning ("Redefined text antiquotation " ^ kind ^ ": " ^ quote name);
2.65 + Symtab.update (name, x) tab);
2.66 +
2.67 +in
2.68 +
2.69 +val add_commands = Library.change global_commands o fold (add_item "command");
2.70 +val add_options = Library.change global_options o fold (add_item "option");
2.71 +
2.72 +fun command src =
2.73 + let val ((name, _), pos) = Args.dest_src src in
2.74 + (case Symtab.lookup (! global_commands) name of
2.75 + NONE => error ("Unknown text antiquotation command: " ^ quote name ^ Position.str_of pos)
2.76 + | SOME f => transform_failure (curry Antiquote.ANTIQUOTE_FAIL (name, pos)) (f src))
2.77 + end;
2.78 +
2.79 +fun option (name, s) f () =
2.80 + (case Symtab.lookup (! global_options) name of
2.81 + NONE => error ("Unknown text antiquotation option: " ^ quote name)
2.82 + | SOME opt => opt s f ());
2.83 +
2.84 +fun options [] f = f
2.85 + | options (opt :: opts) f = option opt (options opts f);
2.86 +
2.87 +
2.88 +fun print_antiquotations () =
2.89 + [Pretty.big_list "text antiquotation commands:"
2.90 + (map Pretty.str (Symtab.keys (! global_commands))),
2.91 + Pretty.big_list "text antiquotation options:" (map Pretty.str (Symtab.keys (! global_options)))]
2.92 + |> Pretty.chunks |> Pretty.writeln;
2.93 +
2.94 +end;
2.95 +
2.96 +
2.97 +
2.98 +(** syntax of antiquotations **)
2.99 +
2.100 +(* option values *)
2.101 +
2.102 +fun boolean "" = true
2.103 + | boolean "true" = true
2.104 + | boolean "false" = false
2.105 + | boolean s = error ("Bad boolean value: " ^ quote s);
2.106 +
2.107 +fun integer s =
2.108 + let
2.109 + fun int ss =
2.110 + (case Library.read_int ss of (i, []) => i
2.111 + | _ => error ("Bad integer value: " ^ quote s));
2.112 + in (case Symbol.explode s of "-" :: ss => ~ (int ss) | ss => int ss) end;
2.113 +
2.114 +
2.115 +(* args syntax *)
2.116 +
2.117 +fun syntax scan = Args.context_syntax "text antiquotation" scan;
2.118 +
2.119 +fun args scan f src node : string =
2.120 + let
2.121 + val loc = if ! locale = "" then NONE else SOME (! locale);
2.122 + val (x, ctxt) = syntax scan src (Toplevel.presentation_context node loc);
2.123 + in f src ctxt x end;
2.124 +
2.125 +
2.126 +(* outer syntax *)
2.127 +
2.128 +local
2.129 +
2.130 +val property = P.xname -- Scan.optional (P.$$$ "=" |-- P.!!! P.xname) "";
2.131 +val properties = Scan.optional (P.$$$ "[" |-- P.!!! (P.enum "," property --| P.$$$ "]")) [];
2.132 +
2.133 +in
2.134 +
2.135 +val antiq = P.!!! (P.position P.xname -- properties -- P.arguments --| Scan.ahead P.eof)
2.136 + >> (fn (((x, pos), y), z) => (y, Args.src ((x, z), pos)));
2.137 +
2.138 +end;
2.139 +
2.140 +
2.141 +(* eval_antiquote *)
2.142 +
2.143 +val modes = ref ([]: string list);
2.144 +
2.145 +fun eval_antiquote lex node (str, pos) =
2.146 + let
2.147 + fun expand (Antiquote.Text s) = s
2.148 + | expand (Antiquote.Antiq x) =
2.149 + let val (opts, src) = Antiquote.scan_arguments lex antiq x in
2.150 + options opts (fn () => command src node) (); (*preview errors!*)
2.151 + Library.setmp print_mode (! modes @ Latex.modes @ ! print_mode)
2.152 + (Output.no_warnings (options opts (fn () => command src node))) ()
2.153 + end;
2.154 + val ants = Antiquote.scan_antiquotes (str, pos);
2.155 + in
2.156 + if is_none node andalso exists Antiquote.is_antiq ants then
2.157 + error ("Cannot expand text antiquotations at top-level" ^ Position.str_of pos)
2.158 + else implode (map expand ants)
2.159 + end;
2.160 +
2.161 +
2.162 +
2.163 +(** present theory source **)
2.164 +
2.165 +(*NB: arranging white space around command spans is a black art.*)
2.166 +
2.167 +(* presentation tokens *)
2.168 +
2.169 +datatype token =
2.170 + NoToken
2.171 + | BasicToken of T.token
2.172 + | MarkupToken of string * (string * Position.T)
2.173 + | MarkupEnvToken of string * (string * Position.T)
2.174 + | VerbatimToken of string * Position.T;
2.175 +
2.176 +fun output_token lex state =
2.177 + let
2.178 + val eval = eval_antiquote lex (try Toplevel.node_of state)
2.179 + in
2.180 + fn NoToken => ""
2.181 + | BasicToken tok => Latex.output_basic tok
2.182 + | MarkupToken (cmd, txt) => Latex.output_markup cmd (eval txt)
2.183 + | MarkupEnvToken (cmd, txt) => Latex.output_markup_env cmd (eval txt)
2.184 + | VerbatimToken txt => Latex.output_verbatim (eval txt)
2.185 + end;
2.186 +
2.187 +fun basic_token pred (BasicToken tok) = pred tok
2.188 + | basic_token _ _ = false;
2.189 +
2.190 +val improper_token = basic_token (not o T.is_proper);
2.191 +val comment_token = basic_token T.is_comment;
2.192 +val blank_token = basic_token T.is_blank;
2.193 +val newline_token = basic_token T.is_newline;
2.194 +
2.195 +
2.196 +(* command spans *)
2.197 +
2.198 +type command = string * Position.T * string list; (*name, position, tags*)
2.199 +type source = (token * (string * int)) list; (*token, markup flag, meta-comment depth*)
2.200 +
2.201 +datatype span = Span of command * (source * source * source * source) * bool;
2.202 +
2.203 +fun make_span cmd src =
2.204 + let
2.205 + fun take_newline (tok :: toks) =
2.206 + if newline_token (fst tok) then ([tok], toks, true)
2.207 + else ([], tok :: toks, false)
2.208 + | take_newline [] = ([], [], false);
2.209 + val (((src_prefix, src_main), src_suffix1), (src_suffix2, src_appendix, newline)) =
2.210 + src
2.211 + |> take_prefix (improper_token o fst)
2.212 + ||>> take_suffix (improper_token o fst)
2.213 + ||>> take_prefix (comment_token o fst)
2.214 + ||> take_newline;
2.215 + in Span (cmd, (src_prefix, src_main, src_suffix1 @ src_suffix2, src_appendix), newline) end;
2.216 +
2.217 +
2.218 +(* present spans *)
2.219 +
2.220 +local
2.221 +
2.222 +fun err_bad_nesting pos =
2.223 + error ("Bad nesting of commands in presentation" ^ pos);
2.224 +
2.225 +fun edge which f (x: string option, y) =
2.226 + if x = y then I
2.227 + else (case which (x, y) of NONE => I | SOME txt => Buffer.add (f txt));
2.228 +
2.229 +val begin_tag = edge #2 Latex.begin_tag;
2.230 +val end_tag = edge #1 Latex.end_tag;
2.231 +fun open_delim delim e = edge #2 Latex.begin_delim e #> delim #> edge #2 Latex.end_delim e;
2.232 +fun close_delim delim e = edge #1 Latex.begin_delim e #> delim #> edge #1 Latex.end_delim e;
2.233 +
2.234 +in
2.235 +
2.236 +fun present_span lex default_tags span state state'
2.237 + (tag_stack, active_tag, newline, buffer, present_cont) =
2.238 + let
2.239 + val present = fold (fn (tok, (flag, 0)) =>
2.240 + Buffer.add (output_token lex state' tok)
2.241 + #> Buffer.add flag
2.242 + | _ => I);
2.243 +
2.244 + val Span ((cmd_name, cmd_pos, cmd_tags), srcs, span_newline) = span;
2.245 +
2.246 + val (tag, tags) = tag_stack;
2.247 + val tag' = try hd (fold OuterKeyword.update_tags cmd_tags (the_list tag));
2.248 +
2.249 + val active_tag' =
2.250 + if is_some tag' then tag'
2.251 + else if cmd_name = "end" andalso not (Toplevel.is_toplevel state') then NONE
2.252 + else try hd (default_tags cmd_name);
2.253 + val edge = (active_tag, active_tag');
2.254 +
2.255 + val newline' =
2.256 + if is_none active_tag' then span_newline else newline;
2.257 +
2.258 + val nesting = Toplevel.level state' - Toplevel.level state;
2.259 + val tag_stack' =
2.260 + if nesting = 0 andalso not (Toplevel.is_proof state) then tag_stack
2.261 + else if nesting >= 0 then (tag', replicate nesting tag @ tags)
2.262 + else
2.263 + (case Library.drop (~ nesting - 1, tags) of
2.264 + tgs :: tgss => (tgs, tgss)
2.265 + | [] => err_bad_nesting (Position.str_of cmd_pos));
2.266 +
2.267 + val buffer' =
2.268 + buffer
2.269 + |> end_tag edge
2.270 + |> close_delim (fst present_cont) edge
2.271 + |> snd present_cont
2.272 + |> open_delim (present (#1 srcs)) edge
2.273 + |> begin_tag edge
2.274 + |> present (#2 srcs);
2.275 + val present_cont' =
2.276 + if newline then (present (#3 srcs), present (#4 srcs))
2.277 + else (I, present (#3 srcs) #> present (#4 srcs));
2.278 + in (tag_stack', active_tag', newline', buffer', present_cont') end;
2.279 +
2.280 +fun present_trailer ((_, tags), active_tag, _, buffer, present_cont) =
2.281 + if not (null tags) then err_bad_nesting " at end of theory"
2.282 + else
2.283 + buffer
2.284 + |> end_tag (active_tag, NONE)
2.285 + |> close_delim (fst present_cont) (active_tag, NONE)
2.286 + |> snd present_cont;
2.287 +
2.288 +end;
2.289 +
2.290 +
2.291 +(* present_thy *)
2.292 +
2.293 +datatype markup = Markup | MarkupEnv | Verbatim;
2.294 +
2.295 +local
2.296 +
2.297 +val space_proper =
2.298 + Scan.one T.is_blank -- Scan.many T.is_comment -- Scan.one T.is_proper;
2.299 +
2.300 +val is_improper = not o (T.is_proper orf T.is_begin_ignore orf T.is_end_ignore);
2.301 +val improper = Scan.many is_improper;
2.302 +val improper_end = Scan.repeat (Scan.unless space_proper (Scan.one is_improper));
2.303 +val blank_end = Scan.repeat (Scan.unless space_proper (Scan.one T.is_blank));
2.304 +
2.305 +val opt_newline = Scan.option (Scan.one T.is_newline);
2.306 +
2.307 +val ignore =
2.308 + Scan.depend (fn d => opt_newline |-- Scan.one T.is_begin_ignore
2.309 + >> pair (d + 1)) ||
2.310 + Scan.depend (fn d => Scan.one T.is_end_ignore --|
2.311 + (if d = 0 then Scan.fail_with (K "Bad nesting of meta-comments") else opt_newline)
2.312 + >> pair (d - 1));
2.313 +
2.314 +val tag = (improper -- P.$$$ "%" -- improper) |-- P.!!! (P.tag_name --| blank_end);
2.315 +
2.316 +val locale =
2.317 + Scan.option ((P.$$$ "(" -- improper -- P.$$$ "in") |--
2.318 + P.!!! (improper |-- P.xname --| (improper -- P.$$$ ")")));
2.319 +
2.320 +in
2.321 +
2.322 +fun present_thy lex default_tags is_markup trs src =
2.323 + let
2.324 + (* tokens *)
2.325 +
2.326 + val ignored = Scan.state --| ignore
2.327 + >> (fn d => (NONE, (NoToken, ("", d))));
2.328 +
2.329 + fun markup mark mk flag = Scan.peek (fn d =>
2.330 + improper |-- P.position (Scan.one (T.is_kind T.Command andf is_markup mark o T.val_of)) --
2.331 + Scan.repeat tag --
2.332 + P.!!!! ((improper -- locale -- improper) |-- P.position P.text --| improper_end)
2.333 + >> (fn (((tok, pos), tags), txt) =>
2.334 + let val name = T.val_of tok
2.335 + in (SOME (name, pos, tags), (mk (name, txt), (flag, d))) end));
2.336 +
2.337 + val command = Scan.peek (fn d =>
2.338 + P.position (Scan.one (T.is_kind T.Command)) --
2.339 + Scan.repeat tag
2.340 + >> (fn ((tok, pos), tags) =>
2.341 + let val name = T.val_of tok
2.342 + in (SOME (name, pos, tags), (BasicToken tok, (Latex.markup_false, d))) end));
2.343 +
2.344 + val cmt = Scan.peek (fn d =>
2.345 + P.$$$ "--" |-- P.!!!! (improper |-- P.position P.text)
2.346 + >> (fn txt => (NONE, (MarkupToken ("cmt", txt), ("", d)))));
2.347 +
2.348 + val other = Scan.peek (fn d =>
2.349 + Scan.one T.not_eof >> (fn tok => (NONE, (BasicToken tok, ("", d)))));
2.350 +
2.351 + val token =
2.352 + ignored ||
2.353 + markup Markup MarkupToken Latex.markup_true ||
2.354 + markup MarkupEnv MarkupEnvToken Latex.markup_true ||
2.355 + markup Verbatim (VerbatimToken o #2) "" ||
2.356 + command || cmt || other;
2.357 +
2.358 +
2.359 + (* spans *)
2.360 +
2.361 + val stopper =
2.362 + ((NONE, (BasicToken (#1 T.stopper), ("", 0))),
2.363 + fn (_, (BasicToken x, _)) => #2 T.stopper x | _ => false);
2.364 +
2.365 + val cmd = Scan.one (is_some o fst);
2.366 + val non_cmd = Scan.one (is_none o fst andf not o #2 stopper) >> #2;
2.367 +
2.368 + val comments = Scan.many (comment_token o fst o snd);
2.369 + val blank = Scan.one (blank_token o fst o snd);
2.370 + val newline = Scan.one (newline_token o fst o snd);
2.371 + val before_cmd =
2.372 + Scan.option (newline -- comments) --
2.373 + Scan.option (newline -- comments) --
2.374 + Scan.option (blank -- comments) -- cmd;
2.375 +
2.376 + val span =
2.377 + Scan.repeat non_cmd -- cmd --
2.378 + Scan.repeat (Scan.unless before_cmd non_cmd) --
2.379 + Scan.option (newline >> (single o snd))
2.380 + >> (fn (((toks1, (cmd, tok2)), toks3), tok4) =>
2.381 + make_span (the cmd) (toks1 @ (tok2 :: (toks3 @ the_default [] tok4))));
2.382 +
2.383 + val spans =
2.384 + src
2.385 + |> Source.filter (not o T.is_semicolon)
2.386 + |> Source.source' 0 T.stopper (Scan.error (Scan.bulk token)) NONE
2.387 + |> Source.source stopper (Scan.error (Scan.bulk span)) NONE
2.388 + |> Source.exhaust;
2.389 + in
2.390 + if length trs = length spans then
2.391 + ((NONE, []), NONE, true, Buffer.empty, (I, I))
2.392 + |> Toplevel.present_excursion (trs ~~ map (present_span lex default_tags) spans)
2.393 + |> present_trailer
2.394 + else error "Messed-up outer syntax for presentation"
2.395 + end;
2.396 +
2.397 +end;
2.398 +
2.399 +
2.400 +
2.401 +(** setup default output **)
2.402 +
2.403 +(* options *)
2.404 +
2.405 +val _ = add_options
2.406 + [("show_types", Library.setmp Syntax.show_types o boolean),
2.407 + ("show_sorts", Library.setmp Syntax.show_sorts o boolean),
2.408 + ("show_structs", Library.setmp show_structs o boolean),
2.409 + ("show_question_marks", Library.setmp show_question_marks o boolean),
2.410 + ("long_names", Library.setmp NameSpace.long_names o boolean),
2.411 + ("short_names", Library.setmp NameSpace.short_names o boolean),
2.412 + ("unique_names", Library.setmp NameSpace.unique_names o boolean),
2.413 + ("eta_contract", Library.setmp Syntax.eta_contract o boolean),
2.414 + ("locale", Library.setmp locale),
2.415 + ("display", Library.setmp display o boolean),
2.416 + ("break", Library.setmp break o boolean),
2.417 + ("quotes", Library.setmp quotes o boolean),
2.418 + ("mode", fn s => fn f => fn () => Library.setmp print_mode (s :: ! print_mode) f ()),
2.419 + ("margin", Pretty.setmp_margin o integer),
2.420 + ("indent", Library.setmp indent o integer),
2.421 + ("source", Library.setmp source o boolean),
2.422 + ("goals_limit", Library.setmp goals_limit o integer)];
2.423 +
2.424 +
2.425 +(* basic pretty printing *)
2.426 +
2.427 +val str_of_source = space_implode " " o map Args.string_of o #2 o #1 o Args.dest_src;
2.428 +
2.429 +fun tweak_line s =
2.430 + if ! display then s else Symbol.strip_blanks s;
2.431 +
2.432 +val pretty_text = Pretty.chunks o map Pretty.str o map tweak_line o Library.split_lines;
2.433 +
2.434 +fun pretty_term ctxt = ProofContext.pretty_term ctxt o ProofContext.revert_skolems ctxt;
2.435 +fun pretty_term_abbrev ctxt =
2.436 + ProofContext.pretty_term_abbrev ctxt o ProofContext.revert_skolems ctxt;
2.437 +
2.438 +fun pretty_term_typ ctxt t =
2.439 + ProofContext.pretty_term ctxt (TypeInfer.constrain t (Term.fastype_of t));
2.440 +
2.441 +fun pretty_term_typeof ctxt = ProofContext.pretty_typ ctxt o Term.fastype_of;
2.442 +
2.443 +fun pretty_term_const ctxt t =
2.444 + if Term.is_Const t then pretty_term ctxt t
2.445 + else error ("Logical constant expected: " ^ ProofContext.string_of_term ctxt t);
2.446 +
2.447 +fun pretty_abbrev ctxt t =
2.448 + let
2.449 + fun err () = error ("Abbreviated constant expected: " ^ ProofContext.string_of_term ctxt t);
2.450 + val (head, args) = Term.strip_comb t;
2.451 + val (c, T) = Term.dest_Const head handle TERM _ => err ();
2.452 + val (U, (u, _)) = Consts.the_abbreviation (ProofContext.consts_of ctxt) c
2.453 + handle TYPE _ => err ();
2.454 + val t' = Term.betapplys (Envir.expand_atom T (U, u), args);
2.455 + in pretty_term_abbrev ctxt (Logic.mk_equals (t, t')) end;
2.456 +
2.457 +fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
2.458 +
2.459 +fun pretty_term_style ctxt (name, t) =
2.460 + pretty_term ctxt (TermStyle.the_style (ProofContext.theory_of ctxt) name ctxt t);
2.461 +
2.462 +fun pretty_thm_style ctxt (name, th) =
2.463 + pretty_term_style ctxt (name, Thm.full_prop_of th);
2.464 +
2.465 +fun pretty_prf full ctxt thms =
2.466 + Pretty.chunks (map (ProofContext.pretty_proof_of ctxt full) thms);
2.467 +
2.468 +fun pretty_theory ctxt name =
2.469 + (Theory.requires (ProofContext.theory_of ctxt) name "presentation"; Pretty.str name);
2.470 +
2.471 +
2.472 +(* Isar output *)
2.473 +
2.474 +fun output_list pretty src ctxt xs =
2.475 + map (pretty ctxt) xs (*always pretty in order to exhibit errors!*)
2.476 + |> (if ! source then K [pretty_text (str_of_source src)] else I)
2.477 + |> (if ! quotes then map Pretty.quote else I)
2.478 + |> (if ! display then
2.479 + map (Output.output o Pretty.string_of o Pretty.indent (! indent))
2.480 + #> space_implode "\\isasep\\isanewline%\n"
2.481 + #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
2.482 + else
2.483 + map (Output.output o (if ! break then Pretty.string_of else Pretty.str_of))
2.484 + #> space_implode "\\isasep\\isanewline%\n"
2.485 + #> enclose "\\isa{" "}");
2.486 +
2.487 +fun output pretty src ctxt = output_list pretty src ctxt o single;
2.488 +
2.489 +fun proof_state node =
2.490 + (case Option.map Toplevel.proof_node node of
2.491 + SOME (SOME prf) => ProofHistory.current prf
2.492 + | _ => error "No proof state");
2.493 +
2.494 +fun output_goals main_goal src node = args (Scan.succeed ()) (output (fn _ => fn _ =>
2.495 + Pretty.chunks (Proof.pretty_goals main_goal (proof_state node)))) src node;
2.496 +
2.497 +fun ml_val txt = "fn _ => (" ^ txt ^ ");";
2.498 +fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option;";
2.499 +fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;"
2.500 +
2.501 +fun output_ml ml src ctxt txt =
2.502 + (ML_Context.use_mltext (ml txt) false (SOME (Context.Proof ctxt));
2.503 + (if ! source then str_of_source src else txt)
2.504 + |> (if ! quotes then quote else I)
2.505 + |> (if ! display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
2.506 + else
2.507 + split_lines
2.508 + #> map (space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|")
2.509 + #> space_implode "\\isasep\\isanewline%\n"));
2.510 +
2.511 +
2.512 +(* commands *)
2.513 +
2.514 +val _ = add_commands
2.515 + [("thm", args Attrib.thms (output_list pretty_thm)),
2.516 + ("thm_style", args (Scan.lift Args.liberal_name -- Attrib.thm) (output pretty_thm_style)),
2.517 + ("prop", args Args.prop (output pretty_term)),
2.518 + ("term", args Args.term (output pretty_term)),
2.519 + ("term_style", args (Scan.lift Args.liberal_name -- Args.term) (output pretty_term_style)),
2.520 + ("term_type", args Args.term (output pretty_term_typ)),
2.521 + ("typeof", args Args.term (output pretty_term_typeof)),
2.522 + ("const", args Args.term (output pretty_term_const)),
2.523 + ("abbrev", args Args.term_abbrev (output pretty_abbrev)),
2.524 + ("typ", args Args.typ_abbrev (output ProofContext.pretty_typ)),
2.525 + ("text", args (Scan.lift Args.name) (output (K pretty_text))),
2.526 + ("goals", output_goals true),
2.527 + ("subgoals", output_goals false),
2.528 + ("prf", args Attrib.thms (output (pretty_prf false))),
2.529 + ("full_prf", args Attrib.thms (output (pretty_prf true))),
2.530 + ("theory", args (Scan.lift Args.name) (output pretty_theory)),
2.531 + ("ML", args (Scan.lift Args.name) (output_ml ml_val)),
2.532 + ("ML_type", args (Scan.lift Args.name) (output_ml ml_type)),
2.533 + ("ML_struct", args (Scan.lift Args.name) (output_ml ml_struct))];
2.534 +
2.535 +end;