src/Pure/Isar/proof_display.ML
author blanchet
Fri, 01 Aug 2014 14:43:57 +0200
changeset 57743 0af2d5dfb0ac
parent 57605 8e0a7eaffe47
child 59184 830bb7ddb3ab
permissions -rw-r--r--
pushing skolems under 'iff' sometimes breaks things further down the proof (as was to be feared)
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
57605
8e0a7eaffe47 tuned messages;
wenzelm
parents: 56932
diff changeset
    15
  val pretty_theorems_diff: bool -> theory list -> theory -> Pretty.T list
8e0a7eaffe47 tuned messages;
wenzelm
parents: 56932
diff changeset
    16
  val pretty_theorems: bool -> theory -> Pretty.T list
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
56932
11a4001b06c6 more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents: 56897
diff changeset
    25
  val print_results: bool -> Position.T -> Proof.context ->
11a4001b06c6 more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents: 56897
diff changeset
    26
    ((string * string) * (string * thm list) list) -> unit
11a4001b06c6 more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents: 56897
diff changeset
    27
  val print_consts: bool -> Position.T -> Proof.context ->
11a4001b06c6 more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents: 56897
diff changeset
    28
    (string * typ -> bool) -> (string * typ) list -> unit
17369
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    29
end
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    30
33389
bb3a5fa94a91 modernized structure Proof_Display;
wenzelm
parents: 32145
diff changeset
    31
structure Proof_Display: PROOF_DISPLAY =
17369
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    32
struct
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    33
20235
3cbf73ed92f8 ProofContext.legacy_pretty_thm;
wenzelm
parents: 20211
diff changeset
    34
(* toplevel pretty printing *)
20211
c7f907f41f7c moved pprint functions to Isar/proof_display.ML;
wenzelm
parents: 19482
diff changeset
    35
30628
4078276bcace removed obsolete pprint operations;
wenzelm
parents: 30364
diff changeset
    36
fun pp_context ctxt =
42717
0bbb56867091 proper configuration options Proof_Context.debug and Proof_Context.verbose;
wenzelm
parents: 42360
diff changeset
    37
 (if Config.get ctxt Proof_Context.debug then
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 41551
diff changeset
    38
    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
    39
  else Pretty.str "<context>");
c7f907f41f7c moved pprint functions to Isar/proof_display.ML;
wenzelm
parents: 19482
diff changeset
    40
45269
6f8949e6c71a more robust ML pretty printing (cf. b6c527c64789);
wenzelm
parents: 44240
diff changeset
    41
fun default_context thy0 =
6f8949e6c71a more robust ML pretty printing (cf. b6c527c64789);
wenzelm
parents: 44240
diff changeset
    42
  (case Context.thread_data () of
6f8949e6c71a more robust ML pretty printing (cf. b6c527c64789);
wenzelm
parents: 44240
diff changeset
    43
    SOME (Context.Proof ctxt) => ctxt
6f8949e6c71a more robust ML pretty printing (cf. b6c527c64789);
wenzelm
parents: 44240
diff changeset
    44
  | SOME (Context.Theory thy) =>
6f8949e6c71a more robust ML pretty printing (cf. b6c527c64789);
wenzelm
parents: 44240
diff changeset
    45
      (case try Syntax.init_pretty_global thy of
6f8949e6c71a more robust ML pretty printing (cf. b6c527c64789);
wenzelm
parents: 44240
diff changeset
    46
        SOME ctxt => ctxt
6f8949e6c71a more robust ML pretty printing (cf. b6c527c64789);
wenzelm
parents: 44240
diff changeset
    47
      | NONE => Syntax.init_pretty_global thy0)
6f8949e6c71a more robust ML pretty printing (cf. b6c527c64789);
wenzelm
parents: 44240
diff changeset
    48
  | NONE => Syntax.init_pretty_global thy0);
44240
4b1a63678839 improved default context for ML toplevel pretty-printing;
wenzelm
parents: 44192
diff changeset
    49
30628
4078276bcace removed obsolete pprint operations;
wenzelm
parents: 30364
diff changeset
    50
fun pp_thm th =
50126
3dec88149176 theorem status about oracles/futures is no longer printed by default;
wenzelm
parents: 49867
diff changeset
    51
  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
    52
  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
    53
44240
4b1a63678839 improved default context for ML toplevel pretty-printing;
wenzelm
parents: 44192
diff changeset
    54
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
    55
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
    56
4078276bcace removed obsolete pprint operations;
wenzelm
parents: 30364
diff changeset
    57
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
    58
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
    59
19432
cae7cc072994 added print_theorems/theory, print_theorems_diff (from pure_thy.ML);
wenzelm
parents: 18799
diff changeset
    60
cae7cc072994 added print_theorems/theory, print_theorems_diff (from pure_thy.ML);
wenzelm
parents: 18799
diff changeset
    61
(* theorems and theory *)
cae7cc072994 added print_theorems/theory, print_theorems_diff (from pure_thy.ML);
wenzelm
parents: 18799
diff changeset
    62
33515
d066e8369a33 print_theorems: suppress concealed (global) facts, unless "!" option is given;
wenzelm
parents: 33389
diff changeset
    63
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
    64
  let
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 41551
diff changeset
    65
    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
    66
    val facts = Global_Theory.facts_of thy;
56158
c2c6d560e7b2 more explicit treatment of verbose mode, which includes concealed entries;
wenzelm
parents: 55763
diff changeset
    67
    val thmss = Facts.dest_static verbose (map Global_Theory.facts_of prev_thys) facts;
57605
8e0a7eaffe47 tuned messages;
wenzelm
parents: 56932
diff changeset
    68
    val prts = map #1 (sort_wrt (#1 o #2) (map (`pretty_fact) thmss));
8e0a7eaffe47 tuned messages;
wenzelm
parents: 56932
diff changeset
    69
  in if null prts then [] else [Pretty.big_list "theorems:" prts] end;
19432
cae7cc072994 added print_theorems/theory, print_theorems_diff (from pure_thy.ML);
wenzelm
parents: 18799
diff changeset
    70
56868
b5fb264d53ba clarified print operations for "terms" and "theorems";
wenzelm
parents: 56158
diff changeset
    71
fun pretty_theorems verbose thy =
b5fb264d53ba clarified print operations for "terms" and "theorems";
wenzelm
parents: 56158
diff changeset
    72
  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
    73
22872
d7189dc8939c tuned ProofDisplay.pretty_full_theory;
wenzelm
parents: 22335
diff changeset
    74
fun pretty_full_theory verbose thy =
57605
8e0a7eaffe47 tuned messages;
wenzelm
parents: 56932
diff changeset
    75
  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
    76
22872
d7189dc8939c tuned ProofDisplay.pretty_full_theory;
wenzelm
parents: 22335
diff changeset
    77
val print_theory = Pretty.writeln o pretty_full_theory false;
22335
6c4204df6863 pretty_full_theory: expose in signature.
aspinall
parents: 22095
diff changeset
    78
19432
cae7cc072994 added print_theorems/theory, print_theorems_diff (from pure_thy.ML);
wenzelm
parents: 18799
diff changeset
    79
17369
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    80
(* refinement rule *)
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    81
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    82
fun pretty_rule ctxt s thm =
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    83
  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
    84
    Pretty.fbrk, Display.pretty_thm ctxt thm];
17369
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    85
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    86
val string_of_rule = Pretty.string_of ooo pretty_rule;
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    87
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
    88
49860
9a0fe50e4534 further attempts to unify/simplify goal output;
wenzelm
parents: 46728
diff changeset
    89
(* goals *)
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
local
9a0fe50e4534 further attempts to unify/simplify goal output;
wenzelm
parents: 46728
diff changeset
    92
9a0fe50e4534 further attempts to unify/simplify goal output;
wenzelm
parents: 46728
diff changeset
    93
fun subgoals 0 = []
9a0fe50e4534 further attempts to unify/simplify goal output;
wenzelm
parents: 46728
diff changeset
    94
  | subgoals 1 = [Pretty.brk 1, Pretty.str "(1 subgoal)"]
9a0fe50e4534 further attempts to unify/simplify goal output;
wenzelm
parents: 46728
diff changeset
    95
  | 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
    96
9a0fe50e4534 further attempts to unify/simplify goal output;
wenzelm
parents: 46728
diff changeset
    97
in
9a0fe50e4534 further attempts to unify/simplify goal output;
wenzelm
parents: 46728
diff changeset
    98
9a0fe50e4534 further attempts to unify/simplify goal output;
wenzelm
parents: 46728
diff changeset
    99
fun pretty_goal_header goal =
55763
4b3907cb5654 tuned signature;
wenzelm
parents: 51958
diff changeset
   100
  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
   101
9a0fe50e4534 further attempts to unify/simplify goal output;
wenzelm
parents: 46728
diff changeset
   102
end;
9a0fe50e4534 further attempts to unify/simplify goal output;
wenzelm
parents: 46728
diff changeset
   103
9a0fe50e4534 further attempts to unify/simplify goal output;
wenzelm
parents: 46728
diff changeset
   104
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
   105
  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
   106
9a0fe50e4534 further attempts to unify/simplify goal output;
wenzelm
parents: 46728
diff changeset
   107
51584
98029ceda8ce more item markup;
wenzelm
parents: 50126
diff changeset
   108
(* goal facts *)
98029ceda8ce more item markup;
wenzelm
parents: 50126
diff changeset
   109
98029ceda8ce more item markup;
wenzelm
parents: 50126
diff changeset
   110
fun pretty_goal_facts ctxt s ths =
98029ceda8ce more item markup;
wenzelm
parents: 50126
diff changeset
   111
  (Pretty.block o Pretty.fbreaks)
51601
8e80ecfa3652 tuned output -- less bullets;
wenzelm
parents: 51584
diff changeset
   112
    [if s = "" then Pretty.str "this:"
55763
4b3907cb5654 tuned signature;
wenzelm
parents: 51958
diff changeset
   113
     else Pretty.block [Pretty.keyword1 s, Pretty.brk 1, Pretty.str "this:"],
51601
8e80ecfa3652 tuned output -- less bullets;
wenzelm
parents: 51584
diff changeset
   114
     Proof_Context.pretty_fact ctxt ("", ths)];
51584
98029ceda8ce more item markup;
wenzelm
parents: 50126
diff changeset
   115
98029ceda8ce more item markup;
wenzelm
parents: 50126
diff changeset
   116
49860
9a0fe50e4534 further attempts to unify/simplify goal output;
wenzelm
parents: 46728
diff changeset
   117
(* method_error *)
9a0fe50e4534 further attempts to unify/simplify goal output;
wenzelm
parents: 46728
diff changeset
   118
49866
619acbd72664 more proof method text position information;
wenzelm
parents: 49863
diff changeset
   119
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
   120
  let
49866
619acbd72664 more proof method text position information;
wenzelm
parents: 49863
diff changeset
   121
    val pr_header =
619acbd72664 more proof method text position information;
wenzelm
parents: 49863
diff changeset
   122
      "Failed to apply " ^ (if kind = "" then "" else kind ^ " ") ^
619acbd72664 more proof method text position information;
wenzelm
parents: 49863
diff changeset
   123
      "proof method" ^ Position.here pos ^ ":\n";
49860
9a0fe50e4534 further attempts to unify/simplify goal output;
wenzelm
parents: 46728
diff changeset
   124
    val pr_facts =
9a0fe50e4534 further attempts to unify/simplify goal output;
wenzelm
parents: 46728
diff changeset
   125
      if null facts then ""
51584
98029ceda8ce more item markup;
wenzelm
parents: 50126
diff changeset
   126
      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
   127
    val pr_goal = string_of_goal ctxt goal;
9a0fe50e4534 further attempts to unify/simplify goal output;
wenzelm
parents: 46728
diff changeset
   128
  in pr_header ^ pr_facts ^ pr_goal end);
9a0fe50e4534 further attempts to unify/simplify goal output;
wenzelm
parents: 46728
diff changeset
   129
9a0fe50e4534 further attempts to unify/simplify goal output;
wenzelm
parents: 46728
diff changeset
   130
17369
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
   131
(* results *)
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
   132
56932
11a4001b06c6 more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents: 56897
diff changeset
   133
fun position_markup pos = Pretty.mark (Position.markup pos Markup.position);
11a4001b06c6 more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents: 56897
diff changeset
   134
28092
5886e9359aa8 no pervasive bindings;
wenzelm
parents: 28087
diff changeset
   135
local
5886e9359aa8 no pervasive bindings;
wenzelm
parents: 28087
diff changeset
   136
56932
11a4001b06c6 more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents: 56897
diff changeset
   137
fun pretty_fact_name pos (kind, "") = position_markup pos (Pretty.keyword1 kind)
11a4001b06c6 more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents: 56897
diff changeset
   138
  | pretty_fact_name pos (kind, name) =
11a4001b06c6 more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents: 56897
diff changeset
   139
      Pretty.block [position_markup pos (Pretty.keyword1 kind), Pretty.brk 1,
41551
791b139a6c1e tuned markup;
wenzelm
parents: 39557
diff changeset
   140
        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
   141
17369
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
   142
fun pretty_facts ctxt =
55763
4b3907cb5654 tuned signature;
wenzelm
parents: 51958
diff changeset
   143
  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
   144
    map (single o Proof_Context.pretty_fact ctxt);
17369
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
   145
27857
fdf43ffceae0 removed obsolete present_results;
wenzelm
parents: 27176
diff changeset
   146
in
fdf43ffceae0 removed obsolete present_results;
wenzelm
parents: 27176
diff changeset
   147
56932
11a4001b06c6 more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents: 56897
diff changeset
   148
fun print_results do_print pos ctxt ((kind, name), facts) =
33643
b275f26a638b eliminated obsolete "internal" kind -- collapsed to unspecific "";
wenzelm
parents: 33515
diff changeset
   149
  if not do_print orelse kind = "" then ()
28092
5886e9359aa8 no pervasive bindings;
wenzelm
parents: 28087
diff changeset
   150
  else if name = "" then
56897
c668735fb8b5 print results as "state", to avoid intrusion into the source text;
wenzelm
parents: 56894
diff changeset
   151
    (Pretty.writeln o Pretty.mark Markup.state)
56932
11a4001b06c6 more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents: 56897
diff changeset
   152
      (Pretty.block (position_markup pos (Pretty.keyword1 kind) :: Pretty.brk 1 ::
11a4001b06c6 more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents: 56897
diff changeset
   153
        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
   154
  else
56897
c668735fb8b5 print results as "state", to avoid intrusion into the source text;
wenzelm
parents: 56894
diff changeset
   155
    (Pretty.writeln o Pretty.mark Markup.state)
46728
85f8e3932712 display proof results as "state", to suppress odd squiggles in the Prover IDE (see also 9240be8c8c69);
wenzelm
parents: 45269
diff changeset
   156
      (case facts of
56932
11a4001b06c6 more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents: 56897
diff changeset
   157
        [fact] => Pretty.blk (1, [pretty_fact_name pos (kind, name), Pretty.fbrk,
50126
3dec88149176 theorem status about oracles/futures is no longer printed by default;
wenzelm
parents: 49867
diff changeset
   158
          Proof_Context.pretty_fact ctxt fact])
56932
11a4001b06c6 more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents: 56897
diff changeset
   159
      | _ => Pretty.blk (1, [pretty_fact_name pos (kind, name), Pretty.fbrk,
46728
85f8e3932712 display proof results as "state", to suppress odd squiggles in the Prover IDE (see also 9240be8c8c69);
wenzelm
parents: 45269
diff changeset
   160
          Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]));
17369
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
   161
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
   162
end;
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
   163
20889
f625a65bfed5 added pretty_consts (from specification.ML);
wenzelm
parents: 20621
diff changeset
   164
f625a65bfed5 added pretty_consts (from specification.ML);
wenzelm
parents: 20621
diff changeset
   165
(* consts *)
f625a65bfed5 added pretty_consts (from specification.ML);
wenzelm
parents: 20621
diff changeset
   166
f625a65bfed5 added pretty_consts (from specification.ML);
wenzelm
parents: 20621
diff changeset
   167
local
f625a65bfed5 added pretty_consts (from specification.ML);
wenzelm
parents: 20621
diff changeset
   168
f625a65bfed5 added pretty_consts (from specification.ML);
wenzelm
parents: 20621
diff changeset
   169
fun pretty_var ctxt (x, T) =
f625a65bfed5 added pretty_consts (from specification.ML);
wenzelm
parents: 20621
diff changeset
   170
  Pretty.block [Pretty.str x, Pretty.str " ::", Pretty.brk 1,
24920
2a45e400fdad generic Syntax.pretty/string_of operations;
wenzelm
parents: 22872
diff changeset
   171
    Pretty.quote (Syntax.pretty_typ ctxt T)];
20889
f625a65bfed5 added pretty_consts (from specification.ML);
wenzelm
parents: 20621
diff changeset
   172
56932
11a4001b06c6 more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents: 56897
diff changeset
   173
fun pretty_vars pos ctxt kind vs =
11a4001b06c6 more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents: 56897
diff changeset
   174
  Pretty.block (Pretty.fbreaks (position_markup pos (Pretty.str kind) :: map (pretty_var ctxt) vs));
20889
f625a65bfed5 added pretty_consts (from specification.ML);
wenzelm
parents: 20621
diff changeset
   175
56932
11a4001b06c6 more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents: 56897
diff changeset
   176
fun pretty_consts pos ctxt pred cs =
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 41551
diff changeset
   177
  (case filter pred (#1 (Proof_Context.inferred_fixes ctxt)) of
56932
11a4001b06c6 more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents: 56897
diff changeset
   178
    [] => pretty_vars pos ctxt "constants" cs
11a4001b06c6 more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents: 56897
diff changeset
   179
  | ps => Pretty.chunks [pretty_vars pos ctxt "parameters" ps, pretty_vars pos ctxt "constants" cs]);
20889
f625a65bfed5 added pretty_consts (from specification.ML);
wenzelm
parents: 20621
diff changeset
   180
44192
a32ca9165928 less verbosity in batch mode -- spam reduction and notable performance improvement;
wenzelm
parents: 42717
diff changeset
   181
in
a32ca9165928 less verbosity in batch mode -- spam reduction and notable performance improvement;
wenzelm
parents: 42717
diff changeset
   182
56932
11a4001b06c6 more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents: 56897
diff changeset
   183
fun print_consts do_print pos ctxt pred cs =
44192
a32ca9165928 less verbosity in batch mode -- spam reduction and notable performance improvement;
wenzelm
parents: 42717
diff changeset
   184
  if not do_print orelse null cs then ()
56932
11a4001b06c6 more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents: 56897
diff changeset
   185
  else Pretty.writeln (Pretty.mark Markup.state (pretty_consts pos ctxt pred cs));
44192
a32ca9165928 less verbosity in batch mode -- spam reduction and notable performance improvement;
wenzelm
parents: 42717
diff changeset
   186
20889
f625a65bfed5 added pretty_consts (from specification.ML);
wenzelm
parents: 20621
diff changeset
   187
end;
f625a65bfed5 added pretty_consts (from specification.ML);
wenzelm
parents: 20621
diff changeset
   188
17369
dec2ddbb3edf Printing of Isar proof elements etc.
wenzelm
parents:
diff changeset
   189
end;