src/Pure/Isar/proof_display.ML
author wenzelm
Wed, 07 May 2014 11:50:30 +0200
changeset 56894 fa12200276bf
parent 56868 b5fb264d53ba
child 56897 c668735fb8b5
permissions -rw-r--r--
more emphatic output for Proof General;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
17369
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Isar/proof_display.ML
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
     3
19432
cae7cc072994 added print_theorems/theory, print_theorems_diff (from pure_thy.ML);
wenzelm
parents: 18799
diff changeset
     4
Printing of theorems, goals, results etc.
17369
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
     5
*)
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
     6
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
     7
signature PROOF_DISPLAY =
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
     8
sig
30628
4078276bcace removed obsolete pprint operations;
wenzelm
parents: 30364
diff changeset
     9
  val pp_context: Proof.context -> Pretty.T
4078276bcace removed obsolete pprint operations;
wenzelm
parents: 30364
diff changeset
    10
  val pp_thm: thm -> Pretty.T
4078276bcace removed obsolete pprint operations;
wenzelm
parents: 30364
diff changeset
    11
  val pp_typ: theory -> typ -> Pretty.T
4078276bcace removed obsolete pprint operations;
wenzelm
parents: 30364
diff changeset
    12
  val pp_term: theory -> term -> Pretty.T
4078276bcace removed obsolete pprint operations;
wenzelm
parents: 30364
diff changeset
    13
  val pp_ctyp: ctyp -> Pretty.T
4078276bcace removed obsolete pprint operations;
wenzelm
parents: 30364
diff changeset
    14
  val pp_cterm: cterm -> Pretty.T
56868
b5fb264d53ba clarified print operations for "terms" and "theorems";
wenzelm
parents: 56158
diff changeset
    15
  val pretty_theorems_diff: bool -> theory list -> theory -> Pretty.T
b5fb264d53ba clarified print operations for "terms" and "theorems";
wenzelm
parents: 56158
diff changeset
    16
  val pretty_theorems: bool -> theory -> Pretty.T
22335
6c4204df6863 pretty_full_theory: expose in signature.
aspinall
parents: 22095
diff changeset
    17
  val pretty_full_theory: bool -> theory -> Pretty.T
28092
5886e9359aa8 no pervasive bindings;
wenzelm
parents: 28087
diff changeset
    18
  val print_theory: theory -> unit
20311
3666316adad6 moved debug option to proof_display.ML (again);
wenzelm
parents: 20253
diff changeset
    19
  val string_of_rule: Proof.context -> string -> thm -> string
49860
9a0fe50e4534 further attempts to unify/simplify goal output;
wenzelm
parents: 46728
diff changeset
    20
  val pretty_goal_header: thm -> Pretty.T
9a0fe50e4534 further attempts to unify/simplify goal output;
wenzelm
parents: 46728
diff changeset
    21
  val string_of_goal: Proof.context -> thm -> string
51584
98029ceda8ce more item markup;
wenzelm
parents: 50126
diff changeset
    22
  val pretty_goal_facts: Proof.context -> string -> thm list -> Pretty.T
49866
619acbd72664 more proof method text position information;
wenzelm
parents: 49863
diff changeset
    23
  val method_error: string -> Position.T ->
619acbd72664 more proof method text position information;
wenzelm
parents: 49863
diff changeset
    24
    {context: Proof.context, facts: thm list, goal: thm} -> 'a Seq.result
46728
85f8e3932712 display proof results as "state", to suppress odd squiggles in the Prover IDE (see also 9240be8c8c69);
wenzelm
parents: 45269
diff changeset
    25
  val print_results: Markup.T -> bool -> Proof.context ->
85f8e3932712 display proof results as "state", to suppress odd squiggles in the Prover IDE (see also 9240be8c8c69);
wenzelm
parents: 45269
diff changeset
    26
    ((string * string) * (string * thm list) list) -> unit
44192
a32ca9165928 less verbosity in batch mode -- spam reduction and notable performance improvement;
wenzelm
parents: 42717
diff changeset
    27
  val print_consts: bool -> Proof.context -> (string * typ -> bool) -> (string * typ) list -> unit
17369
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    28
end
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    29
33389
bb3a5fa94a91 modernized structure Proof_Display;
wenzelm
parents: 32145
diff changeset
    30
structure Proof_Display: PROOF_DISPLAY =
17369
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    31
struct
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    32
20235
3cbf73ed92f8 ProofContext.legacy_pretty_thm;
wenzelm
parents: 20211
diff changeset
    33
(* toplevel pretty printing *)
20211
c7f907f41f7c moved pprint functions to Isar/proof_display.ML;
wenzelm
parents: 19482
diff changeset
    34
30628
4078276bcace removed obsolete pprint operations;
wenzelm
parents: 30364
diff changeset
    35
fun pp_context ctxt =
42717
0bbb56867091 proper configuration options Proof_Context.debug and Proof_Context.verbose;
wenzelm
parents: 42360
diff changeset
    36
 (if Config.get ctxt Proof_Context.debug then
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 41551
diff changeset
    37
    Pretty.quote (Pretty.big_list "proof context:" (Proof_Context.pretty_context ctxt))
20211
c7f907f41f7c moved pprint functions to Isar/proof_display.ML;
wenzelm
parents: 19482
diff changeset
    38
  else Pretty.str "<context>");
c7f907f41f7c moved pprint functions to Isar/proof_display.ML;
wenzelm
parents: 19482
diff changeset
    39
45269
6f8949e6c71a more robust ML pretty printing (cf. b6c527c64789);
wenzelm
parents: 44240
diff changeset
    40
fun default_context thy0 =
6f8949e6c71a more robust ML pretty printing (cf. b6c527c64789);
wenzelm
parents: 44240
diff changeset
    41
  (case Context.thread_data () of
6f8949e6c71a more robust ML pretty printing (cf. b6c527c64789);
wenzelm
parents: 44240
diff changeset
    42
    SOME (Context.Proof ctxt) => ctxt
6f8949e6c71a more robust ML pretty printing (cf. b6c527c64789);
wenzelm
parents: 44240
diff changeset
    43
  | SOME (Context.Theory thy) =>
6f8949e6c71a more robust ML pretty printing (cf. b6c527c64789);
wenzelm
parents: 44240
diff changeset
    44
      (case try Syntax.init_pretty_global thy of
6f8949e6c71a more robust ML pretty printing (cf. b6c527c64789);
wenzelm
parents: 44240
diff changeset
    45
        SOME ctxt => ctxt
6f8949e6c71a more robust ML pretty printing (cf. b6c527c64789);
wenzelm
parents: 44240
diff changeset
    46
      | NONE => Syntax.init_pretty_global thy0)
6f8949e6c71a more robust ML pretty printing (cf. b6c527c64789);
wenzelm
parents: 44240
diff changeset
    47
  | NONE => Syntax.init_pretty_global thy0);
44240
4b1a63678839 improved default context for ML toplevel pretty-printing;
wenzelm
parents: 44192
diff changeset
    48
30628
4078276bcace removed obsolete pprint operations;
wenzelm
parents: 30364
diff changeset
    49
fun pp_thm th =
50126
3dec88149176 theorem status about oracles/futures is no longer printed by default;
wenzelm
parents: 49867
diff changeset
    50
  let val ctxt = default_context (Thm.theory_of_thm th);
3dec88149176 theorem status about oracles/futures is no longer printed by default;
wenzelm
parents: 49867
diff changeset
    51
  in Display.pretty_thm_raw ctxt {quote = true, show_hyps = false} th end;
20211
c7f907f41f7c moved pprint functions to Isar/proof_display.ML;
wenzelm
parents: 19482
diff changeset
    52
44240
4b1a63678839 improved default context for ML toplevel pretty-printing;
wenzelm
parents: 44192
diff changeset
    53
fun pp_typ thy T = Pretty.quote (Syntax.pretty_typ (default_context thy) T);
4b1a63678839 improved default context for ML toplevel pretty-printing;
wenzelm
parents: 44192
diff changeset
    54
fun pp_term thy t = Pretty.quote (Syntax.pretty_term (default_context thy) t);
30628
4078276bcace removed obsolete pprint operations;
wenzelm
parents: 30364
diff changeset
    55
4078276bcace removed obsolete pprint operations;
wenzelm
parents: 30364
diff changeset
    56
fun pp_ctyp cT = pp_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
4078276bcace removed obsolete pprint operations;
wenzelm
parents: 30364
diff changeset
    57
fun pp_cterm ct = pp_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
20211
c7f907f41f7c moved pprint functions to Isar/proof_display.ML;
wenzelm
parents: 19482
diff changeset
    58
19432
cae7cc072994 added print_theorems/theory, print_theorems_diff (from pure_thy.ML);
wenzelm
parents: 18799
diff changeset
    59
cae7cc072994 added print_theorems/theory, print_theorems_diff (from pure_thy.ML);
wenzelm
parents: 18799
diff changeset
    60
(* theorems and theory *)
cae7cc072994 added print_theorems/theory, print_theorems_diff (from pure_thy.ML);
wenzelm
parents: 18799
diff changeset
    61
33515
d066e8369a33 print_theorems: suppress concealed (global) facts, unless "!" option is given;
wenzelm
parents: 33389
diff changeset
    62
fun pretty_theorems_diff verbose prev_thys thy =
19432
cae7cc072994 added print_theorems/theory, print_theorems_diff (from pure_thy.ML);
wenzelm
parents: 18799
diff changeset
    63
  let
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 41551
diff changeset
    64
    val pretty_fact = Proof_Context.pretty_fact (Proof_Context.init_global thy);
39557
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 39284
diff changeset
    65
    val facts = Global_Theory.facts_of thy;
56158
c2c6d560e7b2 more explicit treatment of verbose mode, which includes concealed entries;
wenzelm
parents: 55763
diff changeset
    66
    val thmss = Facts.dest_static verbose (map Global_Theory.facts_of prev_thys) facts;
28210
c164d1892553 more procise printing of fact names;
wenzelm
parents: 28092
diff changeset
    67
  in Pretty.big_list "theorems:" (map #1 (sort_wrt (#1 o #2) (map (`pretty_fact) thmss))) end;
19432
cae7cc072994 added print_theorems/theory, print_theorems_diff (from pure_thy.ML);
wenzelm
parents: 18799
diff changeset
    68
56868
b5fb264d53ba clarified print operations for "terms" and "theorems";
wenzelm
parents: 56158
diff changeset
    69
fun pretty_theorems verbose thy =
b5fb264d53ba clarified print operations for "terms" and "theorems";
wenzelm
parents: 56158
diff changeset
    70
  pretty_theorems_diff verbose (Theory.parents_of thy) thy;
19432
cae7cc072994 added print_theorems/theory, print_theorems_diff (from pure_thy.ML);
wenzelm
parents: 18799
diff changeset
    71
22872
d7189dc8939c tuned ProofDisplay.pretty_full_theory;
wenzelm
parents: 22335
diff changeset
    72
fun pretty_full_theory verbose thy =
33515
d066e8369a33 print_theorems: suppress concealed (global) facts, unless "!" option is given;
wenzelm
parents: 33389
diff changeset
    73
  Pretty.chunks (Display.pretty_full_theory verbose thy @ [pretty_theorems verbose thy]);
20621
29d57880ba00 'print_theory': bang option for full verbosity;
wenzelm
parents: 20311
diff changeset
    74
22872
d7189dc8939c tuned ProofDisplay.pretty_full_theory;
wenzelm
parents: 22335
diff changeset
    75
val print_theory = Pretty.writeln o pretty_full_theory false;
22335
6c4204df6863 pretty_full_theory: expose in signature.
aspinall
parents: 22095
diff changeset
    76
19432
cae7cc072994 added print_theorems/theory, print_theorems_diff (from pure_thy.ML);
wenzelm
parents: 18799
diff changeset
    77
17369
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    78
(* refinement rule *)
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    79
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    80
fun pretty_rule ctxt s thm =
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    81
  Pretty.block [Pretty.str (s ^ " attempt to solve goal by exported rule:"),
50126
3dec88149176 theorem status about oracles/futures is no longer printed by default;
wenzelm
parents: 49867
diff changeset
    82
    Pretty.fbrk, Display.pretty_thm ctxt thm];
17369
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    83
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    84
val string_of_rule = Pretty.string_of ooo pretty_rule;
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    85
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    86
49860
9a0fe50e4534 further attempts to unify/simplify goal output;
wenzelm
parents: 46728
diff changeset
    87
(* goals *)
9a0fe50e4534 further attempts to unify/simplify goal output;
wenzelm
parents: 46728
diff changeset
    88
9a0fe50e4534 further attempts to unify/simplify goal output;
wenzelm
parents: 46728
diff changeset
    89
local
9a0fe50e4534 further attempts to unify/simplify goal output;
wenzelm
parents: 46728
diff changeset
    90
9a0fe50e4534 further attempts to unify/simplify goal output;
wenzelm
parents: 46728
diff changeset
    91
fun subgoals 0 = []
9a0fe50e4534 further attempts to unify/simplify goal output;
wenzelm
parents: 46728
diff changeset
    92
  | subgoals 1 = [Pretty.brk 1, Pretty.str "(1 subgoal)"]
9a0fe50e4534 further attempts to unify/simplify goal output;
wenzelm
parents: 46728
diff changeset
    93
  | subgoals n = [Pretty.brk 1, Pretty.str ("(" ^ string_of_int n ^ " subgoals)")];
9a0fe50e4534 further attempts to unify/simplify goal output;
wenzelm
parents: 46728
diff changeset
    94
9a0fe50e4534 further attempts to unify/simplify goal output;
wenzelm
parents: 46728
diff changeset
    95
in
9a0fe50e4534 further attempts to unify/simplify goal output;
wenzelm
parents: 46728
diff changeset
    96
9a0fe50e4534 further attempts to unify/simplify goal output;
wenzelm
parents: 46728
diff changeset
    97
fun pretty_goal_header goal =
55763
4b3907cb5654 tuned signature;
wenzelm
parents: 51958
diff changeset
    98
  Pretty.block ([Pretty.keyword1 "goal"] @ subgoals (Thm.nprems_of goal) @ [Pretty.str ":"]);
49860
9a0fe50e4534 further attempts to unify/simplify goal output;
wenzelm
parents: 46728
diff changeset
    99
9a0fe50e4534 further attempts to unify/simplify goal output;
wenzelm
parents: 46728
diff changeset
   100
end;
9a0fe50e4534 further attempts to unify/simplify goal output;
wenzelm
parents: 46728
diff changeset
   101
9a0fe50e4534 further attempts to unify/simplify goal output;
wenzelm
parents: 46728
diff changeset
   102
fun string_of_goal ctxt goal =
51958
bca32217b304 retain goal display options when printing error messages, to avoid breakdown for huge goals;
wenzelm
parents: 51601
diff changeset
   103
  Pretty.string_of (Pretty.chunks [pretty_goal_header goal, Goal_Display.pretty_goal ctxt goal]);
49860
9a0fe50e4534 further attempts to unify/simplify goal output;
wenzelm
parents: 46728
diff changeset
   104
9a0fe50e4534 further attempts to unify/simplify goal output;
wenzelm
parents: 46728
diff changeset
   105
51584
98029ceda8ce more item markup;
wenzelm
parents: 50126
diff changeset
   106
(* goal facts *)
98029ceda8ce more item markup;
wenzelm
parents: 50126
diff changeset
   107
98029ceda8ce more item markup;
wenzelm
parents: 50126
diff changeset
   108
fun pretty_goal_facts ctxt s ths =
98029ceda8ce more item markup;
wenzelm
parents: 50126
diff changeset
   109
  (Pretty.block o Pretty.fbreaks)
51601
8e80ecfa3652 tuned output -- less bullets;
wenzelm
parents: 51584
diff changeset
   110
    [if s = "" then Pretty.str "this:"
55763
4b3907cb5654 tuned signature;
wenzelm
parents: 51958
diff changeset
   111
     else Pretty.block [Pretty.keyword1 s, Pretty.brk 1, Pretty.str "this:"],
51601
8e80ecfa3652 tuned output -- less bullets;
wenzelm
parents: 51584
diff changeset
   112
     Proof_Context.pretty_fact ctxt ("", ths)];
51584
98029ceda8ce more item markup;
wenzelm
parents: 50126
diff changeset
   113
98029ceda8ce more item markup;
wenzelm
parents: 50126
diff changeset
   114
49860
9a0fe50e4534 further attempts to unify/simplify goal output;
wenzelm
parents: 46728
diff changeset
   115
(* method_error *)
9a0fe50e4534 further attempts to unify/simplify goal output;
wenzelm
parents: 46728
diff changeset
   116
49866
619acbd72664 more proof method text position information;
wenzelm
parents: 49863
diff changeset
   117
fun method_error kind pos {context = ctxt, facts, goal} = Seq.Error (fn () =>
49860
9a0fe50e4534 further attempts to unify/simplify goal output;
wenzelm
parents: 46728
diff changeset
   118
  let
49866
619acbd72664 more proof method text position information;
wenzelm
parents: 49863
diff changeset
   119
    val pr_header =
619acbd72664 more proof method text position information;
wenzelm
parents: 49863
diff changeset
   120
      "Failed to apply " ^ (if kind = "" then "" else kind ^ " ") ^
619acbd72664 more proof method text position information;
wenzelm
parents: 49863
diff changeset
   121
      "proof method" ^ Position.here pos ^ ":\n";
49860
9a0fe50e4534 further attempts to unify/simplify goal output;
wenzelm
parents: 46728
diff changeset
   122
    val pr_facts =
9a0fe50e4534 further attempts to unify/simplify goal output;
wenzelm
parents: 46728
diff changeset
   123
      if null facts then ""
51584
98029ceda8ce more item markup;
wenzelm
parents: 50126
diff changeset
   124
      else Pretty.string_of (pretty_goal_facts ctxt "using" facts) ^ "\n";
49860
9a0fe50e4534 further attempts to unify/simplify goal output;
wenzelm
parents: 46728
diff changeset
   125
    val pr_goal = string_of_goal ctxt goal;
9a0fe50e4534 further attempts to unify/simplify goal output;
wenzelm
parents: 46728
diff changeset
   126
  in pr_header ^ pr_facts ^ pr_goal end);
9a0fe50e4534 further attempts to unify/simplify goal output;
wenzelm
parents: 46728
diff changeset
   127
9a0fe50e4534 further attempts to unify/simplify goal output;
wenzelm
parents: 46728
diff changeset
   128
17369
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
   129
(* results *)
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
   130
28092
5886e9359aa8 no pervasive bindings;
wenzelm
parents: 28087
diff changeset
   131
local
5886e9359aa8 no pervasive bindings;
wenzelm
parents: 28087
diff changeset
   132
55763
4b3907cb5654 tuned signature;
wenzelm
parents: 51958
diff changeset
   133
fun pretty_fact_name (kind, "") = Pretty.keyword1 kind
41551
791b139a6c1e tuned markup;
wenzelm
parents: 39557
diff changeset
   134
  | pretty_fact_name (kind, name) =
55763
4b3907cb5654 tuned signature;
wenzelm
parents: 51958
diff changeset
   135
      Pretty.block [Pretty.keyword1 kind, Pretty.brk 1,
41551
791b139a6c1e tuned markup;
wenzelm
parents: 39557
diff changeset
   136
        Pretty.str (Long_Name.base_name name), Pretty.str ":"];
28087
a9cccdd9d521 pretty_fact/results: display base only, since results now come with full names (note that Facts.extern is not really well-defined unless we present the real target context);
wenzelm
parents: 27857
diff changeset
   137
17369
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
   138
fun pretty_facts ctxt =
55763
4b3907cb5654 tuned signature;
wenzelm
parents: 51958
diff changeset
   139
  flat o (separate [Pretty.fbrk, Pretty.keyword2 "and", Pretty.str " "]) o
50126
3dec88149176 theorem status about oracles/futures is no longer printed by default;
wenzelm
parents: 49867
diff changeset
   140
    map (single o Proof_Context.pretty_fact ctxt);
17369
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
   141
27857
fdf43ffceae0 removed obsolete present_results;
wenzelm
parents: 27176
diff changeset
   142
in
fdf43ffceae0 removed obsolete present_results;
wenzelm
parents: 27176
diff changeset
   143
46728
85f8e3932712 display proof results as "state", to suppress odd squiggles in the Prover IDE (see also 9240be8c8c69);
wenzelm
parents: 45269
diff changeset
   144
fun print_results markup do_print ctxt ((kind, name), facts) =
33643
b275f26a638b eliminated obsolete "internal" kind -- collapsed to unspecific "";
wenzelm
parents: 33515
diff changeset
   145
  if not do_print orelse kind = "" then ()
28092
5886e9359aa8 no pervasive bindings;
wenzelm
parents: 28087
diff changeset
   146
  else if name = "" then
56894
fa12200276bf more emphatic output for Proof General;
wenzelm
parents: 56868
diff changeset
   147
    (Output.urgent_message o Pretty.string_of o Pretty.mark markup)
55763
4b3907cb5654 tuned signature;
wenzelm
parents: 51958
diff changeset
   148
      (Pretty.block (Pretty.keyword1 kind :: Pretty.brk 1 :: pretty_facts ctxt facts))
46728
85f8e3932712 display proof results as "state", to suppress odd squiggles in the Prover IDE (see also 9240be8c8c69);
wenzelm
parents: 45269
diff changeset
   149
  else
56894
fa12200276bf more emphatic output for Proof General;
wenzelm
parents: 56868
diff changeset
   150
    (Output.urgent_message o Pretty.string_of o Pretty.mark markup)
46728
85f8e3932712 display proof results as "state", to suppress odd squiggles in the Prover IDE (see also 9240be8c8c69);
wenzelm
parents: 45269
diff changeset
   151
      (case facts of
85f8e3932712 display proof results as "state", to suppress odd squiggles in the Prover IDE (see also 9240be8c8c69);
wenzelm
parents: 45269
diff changeset
   152
        [fact] => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
50126
3dec88149176 theorem status about oracles/futures is no longer printed by default;
wenzelm
parents: 49867
diff changeset
   153
          Proof_Context.pretty_fact ctxt fact])
46728
85f8e3932712 display proof results as "state", to suppress odd squiggles in the Prover IDE (see also 9240be8c8c69);
wenzelm
parents: 45269
diff changeset
   154
      | _ => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
85f8e3932712 display proof results as "state", to suppress odd squiggles in the Prover IDE (see also 9240be8c8c69);
wenzelm
parents: 45269
diff changeset
   155
          Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]));
17369
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
   156
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
   157
end;
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
   158
20889
f625a65bfed5 added pretty_consts (from specification.ML);
wenzelm
parents: 20621
diff changeset
   159
f625a65bfed5 added pretty_consts (from specification.ML);
wenzelm
parents: 20621
diff changeset
   160
(* consts *)
f625a65bfed5 added pretty_consts (from specification.ML);
wenzelm
parents: 20621
diff changeset
   161
f625a65bfed5 added pretty_consts (from specification.ML);
wenzelm
parents: 20621
diff changeset
   162
local
f625a65bfed5 added pretty_consts (from specification.ML);
wenzelm
parents: 20621
diff changeset
   163
f625a65bfed5 added pretty_consts (from specification.ML);
wenzelm
parents: 20621
diff changeset
   164
fun pretty_var ctxt (x, T) =
f625a65bfed5 added pretty_consts (from specification.ML);
wenzelm
parents: 20621
diff changeset
   165
  Pretty.block [Pretty.str x, Pretty.str " ::", Pretty.brk 1,
24920
2a45e400fdad generic Syntax.pretty/string_of operations;
wenzelm
parents: 22872
diff changeset
   166
    Pretty.quote (Syntax.pretty_typ ctxt T)];
20889
f625a65bfed5 added pretty_consts (from specification.ML);
wenzelm
parents: 20621
diff changeset
   167
f625a65bfed5 added pretty_consts (from specification.ML);
wenzelm
parents: 20621
diff changeset
   168
fun pretty_vars ctxt kind vs = Pretty.big_list kind (map (pretty_var ctxt) vs);
f625a65bfed5 added pretty_consts (from specification.ML);
wenzelm
parents: 20621
diff changeset
   169
f625a65bfed5 added pretty_consts (from specification.ML);
wenzelm
parents: 20621
diff changeset
   170
fun pretty_consts ctxt pred cs =
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 41551
diff changeset
   171
  (case filter pred (#1 (Proof_Context.inferred_fixes ctxt)) of
20889
f625a65bfed5 added pretty_consts (from specification.ML);
wenzelm
parents: 20621
diff changeset
   172
    [] => pretty_vars ctxt "constants" cs
f625a65bfed5 added pretty_consts (from specification.ML);
wenzelm
parents: 20621
diff changeset
   173
  | ps => Pretty.chunks [pretty_vars ctxt "parameters" ps, pretty_vars ctxt "constants" cs]);
f625a65bfed5 added pretty_consts (from specification.ML);
wenzelm
parents: 20621
diff changeset
   174
44192
a32ca9165928 less verbosity in batch mode -- spam reduction and notable performance improvement;
wenzelm
parents: 42717
diff changeset
   175
in
a32ca9165928 less verbosity in batch mode -- spam reduction and notable performance improvement;
wenzelm
parents: 42717
diff changeset
   176
a32ca9165928 less verbosity in batch mode -- spam reduction and notable performance improvement;
wenzelm
parents: 42717
diff changeset
   177
fun print_consts do_print ctxt pred cs =
a32ca9165928 less verbosity in batch mode -- spam reduction and notable performance improvement;
wenzelm
parents: 42717
diff changeset
   178
  if not do_print orelse null cs then ()
a32ca9165928 less verbosity in batch mode -- spam reduction and notable performance improvement;
wenzelm
parents: 42717
diff changeset
   179
  else Pretty.writeln (pretty_consts ctxt pred cs);
a32ca9165928 less verbosity in batch mode -- spam reduction and notable performance improvement;
wenzelm
parents: 42717
diff changeset
   180
20889
f625a65bfed5 added pretty_consts (from specification.ML);
wenzelm
parents: 20621
diff changeset
   181
end;
f625a65bfed5 added pretty_consts (from specification.ML);
wenzelm
parents: 20621
diff changeset
   182
17369
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
   183
end;