src/Pure/Isar/isar_output.ML
author wenzelm
Thu Apr 07 09:26:48 2005 +0200 (2005-04-07 ago)
changeset 15666 5c5925dc4921
parent 15570 8d8c70b41bab
child 15880 d6aa6c707acf
permissions -rw-r--r--
Scan.peek;
wenzelm@9140
     1
(*  Title:      Pure/Isar/isar_output.ML
wenzelm@9140
     2
    ID:         $Id$
wenzelm@9140
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@9140
     4
wenzelm@9140
     5
Isar theory output.
wenzelm@9140
     6
*)
wenzelm@9140
     7
wenzelm@9140
     8
signature ISAR_OUTPUT =
wenzelm@9140
     9
sig
wenzelm@14899
    10
  val display: bool ref
wenzelm@14899
    11
  val quotes: bool ref
wenzelm@14899
    12
  val indent: int ref
wenzelm@14899
    13
  val source: bool ref
wenzelm@10321
    14
  val add_commands: (string * (Args.src -> Toplevel.state -> string)) list -> unit
wenzelm@9140
    15
  val add_options: (string * (string -> (unit -> string) -> unit -> string)) list -> unit
wenzelm@9220
    16
  val print_antiquotations: unit -> unit
wenzelm@9140
    17
  val boolean: string -> bool
wenzelm@9140
    18
  val integer: string -> int
wenzelm@9140
    19
  val args: (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list)) ->
wenzelm@10321
    20
    (Args.src -> Proof.context -> 'a -> string) -> Args.src -> Toplevel.state -> string
wenzelm@9140
    21
  datatype markup = Markup | MarkupEnv | Verbatim
wenzelm@9140
    22
  val interest_level: int ref
berghofe@15430
    23
  val hide_commands: bool ref
berghofe@15430
    24
  val add_hidden_commands: string list -> unit
wenzelm@11714
    25
  val modes: string list ref
wenzelm@12939
    26
  val eval_antiquote: Scan.lexicon -> Toplevel.state -> string * Position.T -> string
wenzelm@9140
    27
  val parse_thy: (markup -> OuterLex.token list -> OuterLex.token * OuterLex.token list) ->
wenzelm@9140
    28
    Scan.lexicon -> Toplevel.transition list -> (OuterLex.token, 'a) Source.source ->
berghofe@15430
    29
      (Toplevel.transition * (Toplevel.state -> Toplevel.state -> Buffer.T -> Buffer.T)) list * Buffer.T
berghofe@11716
    30
  val output_with: (Proof.context -> 'a -> Pretty.T) -> Args.src ->
berghofe@11716
    31
    Proof.context -> 'a -> string
wenzelm@9140
    32
end;
wenzelm@9140
    33
wenzelm@9140
    34
structure IsarOutput: ISAR_OUTPUT =
wenzelm@9140
    35
struct
wenzelm@9140
    36
wenzelm@9140
    37
structure T = OuterLex;
wenzelm@9140
    38
structure P = OuterParse;
wenzelm@9140
    39
wenzelm@9140
    40
wenzelm@14899
    41
wenzelm@14899
    42
(** global references -- defaults for options **)
wenzelm@14899
    43
wenzelm@14899
    44
val locale = ref "";
wenzelm@14899
    45
val display = ref false;
wenzelm@14899
    46
val quotes = ref false;
wenzelm@14899
    47
val indent = ref 0;
wenzelm@14899
    48
val source = ref false;
wenzelm@14899
    49
val break = ref false;
wenzelm@14899
    50
wenzelm@14899
    51
wenzelm@14899
    52
wenzelm@9140
    53
(** maintain global commands **)
wenzelm@9140
    54
wenzelm@9140
    55
local
wenzelm@9140
    56
wenzelm@9140
    57
val global_commands =
wenzelm@10321
    58
  ref (Symtab.empty: (Args.src -> Toplevel.state -> string) Symtab.table);
wenzelm@9140
    59
wenzelm@9140
    60
val global_options =
wenzelm@9140
    61
  ref (Symtab.empty: (string -> (unit -> string) -> unit -> string) Symtab.table);
wenzelm@9140
    62
wenzelm@9140
    63
wenzelm@9140
    64
fun add_item kind (tab, (name, x)) =
wenzelm@9140
    65
 (if is_none (Symtab.lookup (tab, name)) then ()
wenzelm@9140
    66
  else warning ("Redefined antiquotation output " ^ kind ^ ": " ^ quote name);
wenzelm@9140
    67
  Symtab.update ((name, x), tab));
wenzelm@9140
    68
skalberg@15570
    69
fun add_items kind xs tab = Library.foldl (add_item kind) (tab, xs);
wenzelm@9140
    70
wenzelm@9140
    71
in
wenzelm@9140
    72
wenzelm@9140
    73
val add_commands = Library.change global_commands o (add_items "command");
wenzelm@9140
    74
val add_options = Library.change global_options o (add_items "option");
wenzelm@9140
    75
wenzelm@9140
    76
fun command src =
wenzelm@9140
    77
  let val ((name, _), pos) = Args.dest_src src in
wenzelm@9140
    78
    (case Symtab.lookup (! global_commands, name) of
skalberg@15531
    79
      NONE => error ("Unknown antiquotation command: " ^ quote name ^ Position.str_of pos)
skalberg@15531
    80
    | SOME f => transform_failure (curry Antiquote.ANTIQUOTE_FAIL (name, pos)) (f src))
wenzelm@9140
    81
  end;
wenzelm@9140
    82
wenzelm@9140
    83
fun option (name, s) f () =
wenzelm@9140
    84
  (case Symtab.lookup (! global_options, name) of
skalberg@15531
    85
    NONE => error ("Unknown antiquotation option: " ^ quote name)
skalberg@15531
    86
  | SOME opt => opt s f ());
wenzelm@9140
    87
wenzelm@9140
    88
fun options [] f = f
wenzelm@9140
    89
  | options (opt :: opts) f = option opt (options opts f);
wenzelm@9140
    90
wenzelm@9213
    91
wenzelm@9220
    92
fun print_antiquotations () =
wenzelm@9220
    93
 [Pretty.big_list "antiquotation commands:" (map Pretty.str (Symtab.keys (! global_commands))),
wenzelm@9220
    94
  Pretty.big_list "antiquotation options:" (map Pretty.str (Symtab.keys (! global_options)))]
wenzelm@9220
    95
 |> Pretty.chunks |> Pretty.writeln;
wenzelm@9213
    96
wenzelm@9140
    97
end;
wenzelm@9140
    98
wenzelm@9140
    99
wenzelm@9140
   100
wenzelm@9140
   101
(** syntax of antiquotations **)
wenzelm@9140
   102
wenzelm@9140
   103
(* option values *)
wenzelm@9140
   104
wenzelm@9140
   105
fun boolean "" = true
wenzelm@9140
   106
  | boolean "true" = true
wenzelm@9140
   107
  | boolean "false" = false
wenzelm@9140
   108
  | boolean s = error ("Bad boolean value: " ^ quote s);
wenzelm@9140
   109
wenzelm@9140
   110
fun integer s =
wenzelm@9140
   111
  let
wenzelm@9140
   112
    fun int ss =
wenzelm@14899
   113
      (case Library.read_int ss of (i, []) => i
wenzelm@14899
   114
      | _ => error ("Bad integer value: " ^ quote s));
wenzelm@9140
   115
  in (case Symbol.explode s of "-" :: ss => ~ (int ss) | ss => int ss) end;
wenzelm@9140
   116
wenzelm@9140
   117
wenzelm@9140
   118
(* args syntax *)
wenzelm@9140
   119
wenzelm@9140
   120
fun syntax (scan: (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list))) =
wenzelm@9140
   121
  Args.syntax "antiquotation" scan;
wenzelm@9140
   122
wenzelm@10321
   123
fun args scan f src state : string =
wenzelm@14899
   124
  let
wenzelm@14899
   125
    val ctxt0 =
wenzelm@14899
   126
      if ! locale = "" then Toplevel.context_of state
skalberg@15531
   127
      else #3 (Locale.read_context_statement (SOME (! locale)) [] []
wenzelm@14899
   128
        (ProofContext.init (Toplevel.theory_of state)));
wenzelm@14899
   129
    val (ctxt, x) = syntax scan src ctxt0;
wenzelm@10321
   130
  in f src ctxt x end;
wenzelm@9140
   131
wenzelm@9140
   132
wenzelm@9140
   133
(* outer syntax *)
wenzelm@9140
   134
wenzelm@9140
   135
local
wenzelm@9140
   136
wenzelm@9140
   137
val property = P.xname -- Scan.optional (P.$$$ "=" |-- P.!!! P.xname) "";
wenzelm@9140
   138
val properties = Scan.optional (P.$$$ "[" |-- P.!!! (P.enum "," property --| P.$$$ "]")) [];
wenzelm@9140
   139
wenzelm@9140
   140
val antiq = P.position P.xname -- properties -- P.arguments --| Scan.ahead P.eof
wenzelm@9140
   141
  >> (fn (((x, pos), y), z) => (y, Args.src ((x, z), pos)));
wenzelm@9140
   142
wenzelm@9140
   143
fun antiq_args_aux keyword_lexicon (str, pos) =
wenzelm@9140
   144
  Source.of_string str
wenzelm@9140
   145
  |> Symbol.source false
wenzelm@9140
   146
  |> T.source false (K (keyword_lexicon, Scan.empty_lexicon)) pos
wenzelm@9140
   147
  |> T.source_proper
skalberg@15531
   148
  |> Source.source T.stopper (Scan.error (Scan.bulk (P.!!! antiq))) NONE
wenzelm@9140
   149
  |> Source.exhaust;
wenzelm@9140
   150
wenzelm@9140
   151
in
wenzelm@9140
   152
wenzelm@9140
   153
fun antiq_args lex (s, pos) =
wenzelm@9140
   154
  (case antiq_args_aux lex (s, pos) of [x] => x | _ => raise ERROR) handle ERROR =>
wenzelm@9140
   155
    error ("Malformed antiquotation: " ^ quote ("@{" ^ s ^ "}") ^ Position.str_of pos);
wenzelm@9140
   156
wenzelm@9140
   157
end;
wenzelm@9140
   158
wenzelm@9140
   159
wenzelm@9140
   160
(* eval_antiquote *)
wenzelm@9140
   161
wenzelm@11714
   162
val modes = ref ([]: string list);
wenzelm@11714
   163
wenzelm@9140
   164
fun eval_antiquote lex state (str, pos) =
wenzelm@9140
   165
  let
wenzelm@9140
   166
    fun expand (Antiquote.Text s) = s
wenzelm@9140
   167
      | expand (Antiquote.Antiq x) =
wenzelm@9140
   168
          let val (opts, src) = antiq_args lex x in
wenzelm@10739
   169
            options opts (fn () => command src state) ();  (*preview errors!*)
wenzelm@11714
   170
            Library.setmp print_mode (! modes @ Latex.modes @ ! print_mode)
wenzelm@10570
   171
              (options opts (fn () => command src state)) ()
wenzelm@10321
   172
          end;
wenzelm@9140
   173
    val ants = Antiquote.antiquotes_of (str, pos);
wenzelm@9140
   174
  in
wenzelm@9140
   175
    if Toplevel.is_toplevel state andalso exists Antiquote.is_antiq ants then
wenzelm@9140
   176
      error ("Cannot expand antiquotations at top-level" ^ Position.str_of pos)
wenzelm@9140
   177
    else implode (map expand ants)
wenzelm@9140
   178
  end;
wenzelm@9140
   179
wenzelm@9140
   180
wenzelm@9140
   181
wenzelm@9140
   182
(** present theory source **)
wenzelm@9140
   183
wenzelm@9140
   184
(* present_tokens *)
wenzelm@9140
   185
wenzelm@9140
   186
val interest_level = ref 0;
wenzelm@9140
   187
berghofe@15473
   188
val hide_commands = ref true;
berghofe@15430
   189
val hidden_commands = ref ([] : string list);
berghofe@15430
   190
berghofe@15430
   191
fun add_hidden_commands cmds = (hidden_commands := !hidden_commands @ cmds);
berghofe@15430
   192
berghofe@15430
   193
fun is_proof state = (case Toplevel.node_of state of
berghofe@15430
   194
  Toplevel.Theory _ => false | _ => true) handle Toplevel.UNDEF => false;
berghofe@15430
   195
berghofe@15430
   196
fun is_newline (Latex.Basic tk, _) = T.is_newline tk
berghofe@15430
   197
  | is_newline _ = false;
berghofe@15430
   198
berghofe@15430
   199
fun is_hidden (Latex.Basic tk, _) =
berghofe@15430
   200
      T.is_kind T.Command tk andalso T.val_of tk mem !hidden_commands
berghofe@15430
   201
  | is_hidden _ = false;
berghofe@15430
   202
skalberg@15570
   203
fun filter_newlines toks = (case List.mapPartial
skalberg@15531
   204
    (fn (tk, i) => if is_newline tk then SOME tk else NONE) toks of
berghofe@15529
   205
  [] => [] | [tk] => [tk] | _ :: toks' => toks');
berghofe@15529
   206
berghofe@15437
   207
fun present_tokens lex (flag, toks) state state' =
skalberg@15531
   208
  Buffer.add (case flag of NONE => "" | SOME b => Latex.flag_markup b) o
berghofe@15437
   209
   ((if !hide_commands andalso exists (is_hidden o fst) toks then []
berghofe@15529
   210
     else if !hide_commands andalso is_proof state then
berghofe@15529
   211
       if is_proof state' then [] else filter_newlines toks
skalberg@15570
   212
     else List.mapPartial (fn (tk, i) =>
skalberg@15531
   213
       if i > ! interest_level then NONE else SOME tk) toks)
berghofe@15437
   214
    |> map (apsnd (eval_antiquote lex state'))
wenzelm@11861
   215
    |> Latex.output_tokens
wenzelm@11861
   216
    |> Buffer.add);
wenzelm@9140
   217
wenzelm@9140
   218
wenzelm@9140
   219
(* parse_thy *)
wenzelm@9140
   220
wenzelm@9140
   221
datatype markup = Markup | MarkupEnv | Verbatim;
wenzelm@9140
   222
wenzelm@9140
   223
local
wenzelm@9140
   224
wenzelm@9140
   225
val opt_newline = Scan.option (Scan.one T.is_newline);
wenzelm@9140
   226
wenzelm@9140
   227
fun check_level i =
wenzelm@9140
   228
  if i > 0 then Scan.succeed ()
wenzelm@9140
   229
  else Scan.fail_with (K "Bad nesting of meta-comments");
wenzelm@9140
   230
wenzelm@9140
   231
val ignore =
oheimb@13775
   232
  Scan.depend (fn i => opt_newline |-- P.position (Scan.one T.is_begin_ignore) >> pair (i + 1)) ||
oheimb@13775
   233
  Scan.depend (fn i => P.position (Scan.one T.is_end_ignore) --|
oheimb@13774
   234
    (opt_newline -- check_level i) >> pair (i - 1));
wenzelm@9140
   235
wenzelm@9140
   236
val ignore_cmd = Scan.state -- ignore
skalberg@15531
   237
  >> (fn (i, (x, pos)) => (false, (NONE, ((Latex.Basic x, ("", pos)), i))));
wenzelm@9140
   238
wenzelm@9140
   239
wenzelm@9140
   240
val is_improper = not o (T.is_proper orf T.is_begin_ignore orf T.is_end_ignore);
wenzelm@9140
   241
val improper = Scan.any is_improper;
wenzelm@9140
   242
wenzelm@9140
   243
val improper_keep_indent = Scan.repeat
wenzelm@9140
   244
  (Scan.unless (Scan.one T.is_indent -- Scan.one T.is_proper) (Scan.one is_improper));
wenzelm@9140
   245
wenzelm@9140
   246
val improper_end =
wenzelm@9140
   247
  (improper -- P.semicolon) |-- improper_keep_indent ||
wenzelm@9140
   248
  improper_keep_indent;
wenzelm@9140
   249
wenzelm@9140
   250
wenzelm@9140
   251
val stopper =
skalberg@15531
   252
  ((false, (NONE, ((Latex.Basic (#1 T.stopper), ("", Position.none)), 0))),
wenzelm@11861
   253
    fn (_, (_, ((Latex.Basic x, _), _))) => (#2 T.stopper x) | _ => false);
wenzelm@9140
   254
wenzelm@9140
   255
in
wenzelm@9140
   256
wenzelm@9140
   257
fun parse_thy markup lex trs src =
wenzelm@9140
   258
  let
wenzelm@9140
   259
    val text = P.position P.text;
wenzelm@15666
   260
    val token = Scan.peek (fn i =>
wenzelm@9140
   261
     (improper |-- markup Markup -- P.!!!! (improper |-- text --| improper_end)
skalberg@15531
   262
        >> (fn (x, y) => (true, (SOME true, ((Latex.Markup (T.val_of x), y), i)))) ||
wenzelm@9140
   263
      improper |-- markup MarkupEnv -- P.!!!! (improper |-- text --| improper_end)
skalberg@15531
   264
        >> (fn (x, y) => (true, (SOME true, ((Latex.MarkupEnv (T.val_of x), y), i)))) ||
wenzelm@9140
   265
      (P.$$$ "--" |-- P.!!!! (improper |-- text))
skalberg@15531
   266
        >> (fn y => (false, (NONE, ((Latex.Markup "cmt", y), i)))) ||
wenzelm@9140
   267
      (improper -- markup Verbatim) |-- P.!!!! (improper |-- text --| improper_end)
skalberg@15531
   268
        >> (fn y => (true, (NONE, ((Latex.Verbatim, y), i)))) ||
wenzelm@9140
   269
      P.position (Scan.one T.not_eof)
wenzelm@15666
   270
        >> (fn (x, pos) => (T.is_kind T.Command x, (SOME false, ((Latex.Basic x, ("", pos)), i))))));
wenzelm@9140
   271
wenzelm@9140
   272
    val body = Scan.any (not o fst andf not o #2 stopper);
wenzelm@11861
   273
    val section = body -- Scan.one fst -- body
wenzelm@11861
   274
      >> (fn ((b1, c), b2) => (#1 (#2 c), map (snd o snd) (b1 @ (c :: b2))));
wenzelm@9140
   275
wenzelm@9140
   276
    val cmds =
wenzelm@9140
   277
      src
wenzelm@9140
   278
      |> Source.filter (not o T.is_semicolon)
skalberg@15531
   279
      |> Source.source' 0 T.stopper (Scan.error (Scan.bulk (ignore_cmd || token))) NONE
skalberg@15531
   280
      |> Source.source stopper (Scan.error (Scan.bulk section)) NONE
wenzelm@9140
   281
      |> Source.exhaust;
wenzelm@9140
   282
  in
wenzelm@9140
   283
    if length cmds = length trs then
wenzelm@9140
   284
      (trs ~~ map (present_tokens lex) cmds, Buffer.empty)
wenzelm@11861
   285
    else error "Messed-up outer syntax for presentation"
wenzelm@9140
   286
  end;
wenzelm@9140
   287
wenzelm@9140
   288
end;
wenzelm@9140
   289
wenzelm@9140
   290
wenzelm@9140
   291
wenzelm@9140
   292
(** setup default output **)
wenzelm@9140
   293
wenzelm@9140
   294
(* options *)
wenzelm@9140
   295
wenzelm@9140
   296
val _ = add_options
wenzelm@9220
   297
 [("show_types", Library.setmp Syntax.show_types o boolean),
wenzelm@9220
   298
  ("show_sorts", Library.setmp Syntax.show_sorts o boolean),
wenzelm@14707
   299
  ("show_structs", Library.setmp show_structs o boolean),
berghofe@15473
   300
  ("show_var_qmarks", Library.setmp show_var_qmarks o boolean),
wenzelm@14696
   301
  ("long_names", Library.setmp NameSpace.long_names o boolean),
wenzelm@9220
   302
  ("eta_contract", Library.setmp Syntax.eta_contract o boolean),
wenzelm@14899
   303
  ("locale", Library.setmp locale),
wenzelm@9140
   304
  ("display", Library.setmp display o boolean),
berghofe@13929
   305
  ("break", Library.setmp break o boolean),
wenzelm@9140
   306
  ("quotes", Library.setmp quotes o boolean),
wenzelm@9140
   307
  ("mode", fn s => fn f => fn () => Library.setmp print_mode (s :: ! print_mode) f ()),
wenzelm@9732
   308
  ("margin", Pretty.setmp_margin o integer),
wenzelm@9750
   309
  ("indent", Library.setmp indent o integer),
wenzelm@10321
   310
  ("source", Library.setmp source o boolean),
wenzelm@10321
   311
  ("goals_limit", Library.setmp goals_limit o integer)];
wenzelm@9140
   312
wenzelm@9140
   313
wenzelm@9140
   314
(* commands *)
wenzelm@9140
   315
wenzelm@9140
   316
fun cond_quote prt =
wenzelm@9140
   317
  if ! quotes then Pretty.quote prt else prt;
wenzelm@9140
   318
wenzelm@9140
   319
fun cond_display prt =
wenzelm@9140
   320
  if ! display then
wenzelm@14835
   321
    Output.output (Pretty.string_of (Pretty.indent (! indent) prt))
wenzelm@9863
   322
    |> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
wenzelm@9140
   323
  else
wenzelm@14835
   324
    Output.output ((if ! break then Pretty.string_of else Pretty.str_of) prt)
wenzelm@9140
   325
    |> enclose "\\isa{" "}";
wenzelm@9140
   326
kleing@14345
   327
fun cond_seq_display prts =
kleing@14345
   328
  if ! display then
wenzelm@14835
   329
    map (Output.output o Pretty.string_of o Pretty.indent (! indent)) prts
kleing@14345
   330
    |> separate "\\isasep\\isanewline%\n"
kleing@14345
   331
    |> implode
kleing@14345
   332
    |> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
kleing@14345
   333
  else
wenzelm@14835
   334
    map (Output.output o (if ! break then Pretty.string_of else Pretty.str_of)) prts
kleing@14345
   335
    |> separate "\\isasep\\isanewline%\n"
kleing@14345
   336
    |> implode
kleing@14345
   337
    |> enclose "\\isa{" "}";
kleing@14345
   338
wenzelm@11011
   339
fun tweak_line s =
wenzelm@11011
   340
  if ! display then s else Symbol.strip_blanks s;
wenzelm@9750
   341
wenzelm@11011
   342
val pretty_text = Pretty.chunks o map Pretty.str o map tweak_line o Library.split_lines;
wenzelm@9140
   343
wenzelm@9750
   344
val pretty_source =
wenzelm@9750
   345
  pretty_text o space_implode " " o map Args.string_of o #2 o #1 o Args.dest_src;
wenzelm@9140
   346
wenzelm@12055
   347
fun pretty_term ctxt = ProofContext.pretty_term ctxt o ProofContext.extern_skolem ctxt;
wenzelm@9140
   348
kleing@14345
   349
fun pretty_thm ctxt = pretty_term ctxt o Thm.prop_of;
wenzelm@9140
   350
kleing@15349
   351
fun lhs_of (Const ("==",_) $ t $ _) = t
kleing@15349
   352
  | lhs_of (Const ("Trueprop",_) $ t) = lhs_of t
kleing@15349
   353
  | lhs_of (Const ("==>",_) $ _ $ t) = lhs_of t
kleing@15349
   354
  | lhs_of (_ $ t $ _) = t
kleing@15349
   355
  | lhs_of _ = error ("Binary operator expected")
kleing@15349
   356
kleing@15349
   357
fun pretty_lhs ctxt = pretty_term ctxt o lhs_of o Thm.prop_of;
kleing@15349
   358
kleing@15349
   359
fun rhs_of (Const ("==",_) $ _ $ t) = t
kleing@15349
   360
  | rhs_of (Const ("Trueprop",_) $ t) = rhs_of t
kleing@15349
   361
  | rhs_of (Const ("==>",_) $ _ $ t) = rhs_of t
kleing@15349
   362
  | rhs_of (_ $ _ $ t) = t
kleing@15349
   363
  | rhs_of _ = error ("Binary operator expected")
kleing@15349
   364
kleing@15349
   365
fun pretty_rhs ctxt = pretty_term ctxt o rhs_of o Thm.prop_of;
kleing@15349
   366
wenzelm@12055
   367
fun pretty_prf full ctxt thms =    (* FIXME context syntax!? *)
berghofe@11524
   368
  Pretty.chunks (map (ProofSyntax.pretty_proof_of full) thms);
berghofe@11524
   369
wenzelm@9750
   370
fun output_with pretty src ctxt x =
wenzelm@9750
   371
  let
wenzelm@12055
   372
    val prt = pretty ctxt x;      (*always pretty in order to catch errors!*)
wenzelm@9750
   373
    val prt' = if ! source then pretty_source src else prt;
wenzelm@9750
   374
  in cond_display (cond_quote prt') end;
wenzelm@9732
   375
kleing@14345
   376
fun output_seq_with pretty src ctxt xs =
kleing@14345
   377
  let
kleing@14345
   378
    val prts = map (pretty ctxt) xs;   (*always pretty in order to catch errors!*)
kleing@14345
   379
    val prts' = if ! source then [pretty_source src] else prts;
kleing@14345
   380
  in cond_seq_display (map cond_quote prts') end;
kleing@14345
   381
wenzelm@10360
   382
fun output_goals main_goal src state = args (Scan.succeed ()) (output_with (fn _ => fn _ =>
wenzelm@10360
   383
  Pretty.chunks (Proof.pretty_goals main_goal (Toplevel.proof_of state
wenzelm@10360
   384
      handle Toplevel.UNDEF => error "No proof state")))) src state;
wenzelm@10360
   385
wenzelm@9140
   386
val _ = add_commands
wenzelm@14696
   387
 [("thm", args Attrib.local_thmss (output_seq_with pretty_thm)),
kleing@15349
   388
  ("lhs", args Attrib.local_thmss (output_seq_with pretty_lhs)),
kleing@15349
   389
  ("rhs", args Attrib.local_thmss (output_seq_with pretty_rhs)),
wenzelm@9750
   390
  ("prop", args Args.local_prop (output_with pretty_term)),
wenzelm@9750
   391
  ("term", args Args.local_term (output_with pretty_term)),
wenzelm@14776
   392
  ("typ", args Args.local_typ_raw (output_with ProofContext.pretty_typ)),
wenzelm@14696
   393
  ("text", args (Scan.lift Args.name) (output_with (K pretty_text))),
wenzelm@10360
   394
  ("goals", output_goals true),
wenzelm@14696
   395
  ("subgoals", output_goals false),
wenzelm@14696
   396
  ("prf", args Attrib.local_thmss (output_with (pretty_prf false))),
wenzelm@14696
   397
  ("full_prf", args Attrib.local_thmss (output_with (pretty_prf true)))];
wenzelm@9140
   398
wenzelm@9140
   399
end;