src/Pure/goal_display.ML
author wenzelm
Sun, 25 Nov 2012 19:49:24 +0100
changeset 50201 c26369c9eda6
parent 49847 ed5080c03165
child 50537 08ce81aeeacc
permissions -rw-r--r--
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
32187
cca43ca13f4f renamed structure Display_Goal to Goal_Display;
wenzelm
parents: 32168
diff changeset
     1
(*  Title:      Pure/goal_display.ML
32089
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
     4
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
     5
Display tactical goal state.
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
     6
*)
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
     7
32187
cca43ca13f4f renamed structure Display_Goal to Goal_Display;
wenzelm
parents: 32168
diff changeset
     8
signature GOAL_DISPLAY =
32089
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
     9
sig
39125
f45d332a90e3 pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents: 39118
diff changeset
    10
  val goals_limit_default: int Unsynchronized.ref
39163
4d701c0388c3 more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
wenzelm
parents: 39134
diff changeset
    11
  val goals_limit_raw: Config.raw
39125
f45d332a90e3 pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents: 39118
diff changeset
    12
  val goals_limit: int Config.T
f45d332a90e3 pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents: 39118
diff changeset
    13
  val goals_total: bool Config.T
f45d332a90e3 pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents: 39118
diff changeset
    14
  val show_main_goal_default: bool Unsynchronized.ref
39163
4d701c0388c3 more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
wenzelm
parents: 39134
diff changeset
    15
  val show_main_goal_raw: Config.raw
39125
f45d332a90e3 pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents: 39118
diff changeset
    16
  val show_main_goal: bool Config.T
39050
600de0485859 turned show_consts into proper configuration option;
wenzelm
parents: 33957
diff changeset
    17
  val show_consts_default: bool Unsynchronized.ref
39163
4d701c0388c3 more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
wenzelm
parents: 39134
diff changeset
    18
  val show_consts_raw: Config.raw
39050
600de0485859 turned show_consts into proper configuration option;
wenzelm
parents: 33957
diff changeset
    19
  val show_consts: bool Config.T
32145
220c9e439d39 clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents: 32089
diff changeset
    20
  val pretty_flexpair: Proof.context -> term * term -> Pretty.T
39125
f45d332a90e3 pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents: 39118
diff changeset
    21
  val pretty_goals: Proof.context -> thm -> Pretty.T list
f45d332a90e3 pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents: 39118
diff changeset
    22
  val pretty_goals_without_context: thm -> Pretty.T list
49847
ed5080c03165 some attempts to unify/simplify pretty_goal;
wenzelm
parents: 45666
diff changeset
    23
  val pretty_goal: {main: bool, limit: bool} -> Proof.context -> thm -> Pretty.T
32089
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
    24
end;
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
    25
32187
cca43ca13f4f renamed structure Display_Goal to Goal_Display;
wenzelm
parents: 32168
diff changeset
    26
structure Goal_Display: GOAL_DISPLAY =
32089
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
    27
struct
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
    28
39125
f45d332a90e3 pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents: 39118
diff changeset
    29
val goals_limit_default = Unsynchronized.ref 10;
39163
4d701c0388c3 more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
wenzelm
parents: 39134
diff changeset
    30
val goals_limit_raw = Config.declare "goals_limit" (fn _ => Config.Int (! goals_limit_default));
4d701c0388c3 more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
wenzelm
parents: 39134
diff changeset
    31
val goals_limit = Config.int goals_limit_raw;
39125
f45d332a90e3 pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents: 39118
diff changeset
    32
f45d332a90e3 pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents: 39118
diff changeset
    33
val goals_total = Config.bool (Config.declare "goals_total" (fn _ => Config.Bool true));
39050
600de0485859 turned show_consts into proper configuration option;
wenzelm
parents: 33957
diff changeset
    34
39125
f45d332a90e3 pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents: 39118
diff changeset
    35
val show_main_goal_default = Unsynchronized.ref false;
39163
4d701c0388c3 more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
wenzelm
parents: 39134
diff changeset
    36
val show_main_goal_raw =
39125
f45d332a90e3 pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents: 39118
diff changeset
    37
  Config.declare "show_main_goal" (fn _ => Config.Bool (! show_main_goal_default));
39163
4d701c0388c3 more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
wenzelm
parents: 39134
diff changeset
    38
val show_main_goal = Config.bool show_main_goal_raw;
39125
f45d332a90e3 pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents: 39118
diff changeset
    39
39050
600de0485859 turned show_consts into proper configuration option;
wenzelm
parents: 33957
diff changeset
    40
val show_consts_default = Unsynchronized.ref false;
39163
4d701c0388c3 more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
wenzelm
parents: 39134
diff changeset
    41
val show_consts_raw = Config.declare "show_consts" (fn _ => Config.Bool (! show_consts_default));
4d701c0388c3 more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
wenzelm
parents: 39134
diff changeset
    42
val show_consts = Config.bool show_consts_raw;
32089
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
    43
32145
220c9e439d39 clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents: 32089
diff changeset
    44
fun pretty_flexpair ctxt (t, u) = Pretty.block
220c9e439d39 clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents: 32089
diff changeset
    45
  [Syntax.pretty_term ctxt t, Pretty.str " =?=", Pretty.brk 1, Syntax.pretty_term ctxt u];
32089
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
    46
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
    47
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
    48
(*print thm A1,...,An/B in "goal style" -- premises as numbered subgoals*)
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
    49
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
    50
local
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
    51
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
    52
fun ins_entry (x, y) =
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
    53
  AList.default (op =) (x, []) #>
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
    54
  AList.map_entry (op =) x (insert (op =) y);
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
    55
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
    56
val add_consts = Term.fold_aterms
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
    57
  (fn Const (c, T) => ins_entry (T, (c, T))
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
    58
    | _ => I);
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
    59
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
    60
val add_vars = Term.fold_aterms
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
    61
  (fn Free (x, T) => ins_entry (T, (x, ~1))
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
    62
    | Var (xi, T) => ins_entry (T, xi)
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
    63
    | _ => I);
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
    64
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
    65
val add_varsT = Term.fold_atyps
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
    66
  (fn TFree (x, S) => ins_entry (S, (x, ~1))
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
    67
    | TVar (xi, S) => ins_entry (S, xi)
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
    68
    | _ => I);
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
    69
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
    70
fun sort_idxs vs = map (apsnd (sort (prod_ord string_ord int_ord))) vs;
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
    71
fun sort_cnsts cs = map (apsnd (sort_wrt fst)) cs;
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
    72
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
    73
fun consts_of t = sort_cnsts (add_consts t []);
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
    74
fun vars_of t = sort_idxs (add_vars t []);
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
    75
fun varsT_of t = rev (sort_idxs (Term.fold_types add_varsT t []));
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
    76
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
    77
in
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
    78
39125
f45d332a90e3 pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents: 39118
diff changeset
    79
fun pretty_goals ctxt0 state =
32089
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
    80
  let
39134
917b4b6ba3d2 turned show_sorts/show_types into proper configuration options;
wenzelm
parents: 39125
diff changeset
    81
    val ctxt = ctxt0
917b4b6ba3d2 turned show_sorts/show_types into proper configuration options;
wenzelm
parents: 39125
diff changeset
    82
      |> Config.put show_free_types false
917b4b6ba3d2 turned show_sorts/show_types into proper configuration options;
wenzelm
parents: 39125
diff changeset
    83
      |> Config.put show_types
917b4b6ba3d2 turned show_sorts/show_types into proper configuration options;
wenzelm
parents: 39125
diff changeset
    84
       (Config.get ctxt0 show_types orelse
917b4b6ba3d2 turned show_sorts/show_types into proper configuration options;
wenzelm
parents: 39125
diff changeset
    85
        Config.get ctxt0 show_sorts orelse
917b4b6ba3d2 turned show_sorts/show_types into proper configuration options;
wenzelm
parents: 39125
diff changeset
    86
        Config.get ctxt0 show_all_types)
917b4b6ba3d2 turned show_sorts/show_types into proper configuration options;
wenzelm
parents: 39125
diff changeset
    87
      |> Config.put show_sorts false;
39125
f45d332a90e3 pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents: 39118
diff changeset
    88
39134
917b4b6ba3d2 turned show_sorts/show_types into proper configuration options;
wenzelm
parents: 39125
diff changeset
    89
    val show_sorts0 = Config.get ctxt0 show_sorts;
917b4b6ba3d2 turned show_sorts/show_types into proper configuration options;
wenzelm
parents: 39125
diff changeset
    90
    val show_types = Config.get ctxt show_types;
917b4b6ba3d2 turned show_sorts/show_types into proper configuration options;
wenzelm
parents: 39125
diff changeset
    91
    val show_consts = Config.get ctxt show_consts
917b4b6ba3d2 turned show_sorts/show_types into proper configuration options;
wenzelm
parents: 39125
diff changeset
    92
    val show_main_goal = Config.get ctxt show_main_goal;
39125
f45d332a90e3 pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents: 39118
diff changeset
    93
    val goals_limit = Config.get ctxt goals_limit;
f45d332a90e3 pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents: 39118
diff changeset
    94
    val goals_total = Config.get ctxt goals_total;
39115
a00da1674c1c turned show_no_free_types into proper configuration option show_free_types, with flipped polarity;
wenzelm
parents: 39050
diff changeset
    95
32145
220c9e439d39 clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents: 32089
diff changeset
    96
    val prt_sort = Syntax.pretty_sort ctxt;
220c9e439d39 clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents: 32089
diff changeset
    97
    val prt_typ = Syntax.pretty_typ ctxt;
220c9e439d39 clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents: 32089
diff changeset
    98
    val prt_term = Syntax.pretty_term ctxt;
220c9e439d39 clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents: 32089
diff changeset
    99
32089
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
   100
    fun prt_atoms prt prtT (X, xs) = Pretty.block
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
   101
      [Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::",
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
   102
        Pretty.brk 1, prtT X];
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
   103
32145
220c9e439d39 clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents: 32089
diff changeset
   104
    fun prt_var (x, ~1) = prt_term (Syntax.free x)
220c9e439d39 clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents: 32089
diff changeset
   105
      | prt_var xi = prt_term (Syntax.var xi);
32089
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
   106
32145
220c9e439d39 clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents: 32089
diff changeset
   107
    fun prt_varT (x, ~1) = prt_typ (TFree (x, []))
220c9e439d39 clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents: 32089
diff changeset
   108
      | prt_varT xi = prt_typ (TVar (xi, []));
32089
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
   109
32145
220c9e439d39 clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents: 32089
diff changeset
   110
    val prt_consts = prt_atoms (prt_term o Const) prt_typ;
220c9e439d39 clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents: 32089
diff changeset
   111
    val prt_vars = prt_atoms prt_var prt_typ;
220c9e439d39 clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents: 32089
diff changeset
   112
    val prt_varsT = prt_atoms prt_varT prt_sort;
32089
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
   113
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
   114
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
   115
    fun pretty_list _ _ [] = []
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
   116
      | pretty_list name prt lst = [Pretty.big_list name (map prt lst)];
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
   117
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 39163
diff changeset
   118
    fun pretty_subgoal (n, A) =
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49847
diff changeset
   119
      Pretty.markup Markup.subgoal [Pretty.str (" " ^ string_of_int n ^ ". "), prt_term A];
32089
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
   120
    fun pretty_subgoals As = map pretty_subgoal (1 upto length As ~~ As);
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
   121
32145
220c9e439d39 clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents: 32089
diff changeset
   122
    val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair ctxt);
32089
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
   123
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
   124
    val pretty_consts = pretty_list "constants:" prt_consts o consts_of;
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
   125
    val pretty_vars = pretty_list "variables:" prt_vars o vars_of;
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
   126
    val pretty_varsT = pretty_list "type variables:" prt_varsT o varsT_of;
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
   127
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
   128
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
   129
    val {prop, tpairs, ...} = Thm.rep_thm state;
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
   130
    val (As, B) = Logic.strip_horn prop;
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
   131
    val ngoals = length As;
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
   132
  in
39134
917b4b6ba3d2 turned show_sorts/show_types into proper configuration options;
wenzelm
parents: 39125
diff changeset
   133
    (if show_main_goal then [prt_term B] else []) @
917b4b6ba3d2 turned show_sorts/show_types into proper configuration options;
wenzelm
parents: 39125
diff changeset
   134
     (if ngoals = 0 then [Pretty.str "No subgoals!"]
917b4b6ba3d2 turned show_sorts/show_types into proper configuration options;
wenzelm
parents: 39125
diff changeset
   135
      else if ngoals > goals_limit then
917b4b6ba3d2 turned show_sorts/show_types into proper configuration options;
wenzelm
parents: 39125
diff changeset
   136
        pretty_subgoals (take goals_limit As) @
917b4b6ba3d2 turned show_sorts/show_types into proper configuration options;
wenzelm
parents: 39125
diff changeset
   137
        (if goals_total then [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
917b4b6ba3d2 turned show_sorts/show_types into proper configuration options;
wenzelm
parents: 39125
diff changeset
   138
         else [])
917b4b6ba3d2 turned show_sorts/show_types into proper configuration options;
wenzelm
parents: 39125
diff changeset
   139
      else pretty_subgoals As) @
917b4b6ba3d2 turned show_sorts/show_types into proper configuration options;
wenzelm
parents: 39125
diff changeset
   140
    pretty_ffpairs tpairs @
917b4b6ba3d2 turned show_sorts/show_types into proper configuration options;
wenzelm
parents: 39125
diff changeset
   141
    (if show_consts then pretty_consts prop else []) @
917b4b6ba3d2 turned show_sorts/show_types into proper configuration options;
wenzelm
parents: 39125
diff changeset
   142
    (if show_types then pretty_vars prop else []) @
917b4b6ba3d2 turned show_sorts/show_types into proper configuration options;
wenzelm
parents: 39125
diff changeset
   143
    (if show_sorts0 then pretty_varsT prop else [])
32089
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
   144
  end;
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
   145
39125
f45d332a90e3 pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents: 39118
diff changeset
   146
fun pretty_goals_without_context th =
f45d332a90e3 pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents: 39118
diff changeset
   147
  let val ctxt =
f45d332a90e3 pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents: 39118
diff changeset
   148
    Config.put show_main_goal true (Syntax.init_pretty_global (Thm.theory_of_thm th))
f45d332a90e3 pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents: 39118
diff changeset
   149
  in pretty_goals ctxt th end;
32089
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
   150
49847
ed5080c03165 some attempts to unify/simplify pretty_goal;
wenzelm
parents: 45666
diff changeset
   151
fun pretty_goal {main, limit} ctxt th =
ed5080c03165 some attempts to unify/simplify pretty_goal;
wenzelm
parents: 45666
diff changeset
   152
  Pretty.chunks (pretty_goals
ed5080c03165 some attempts to unify/simplify pretty_goal;
wenzelm
parents: 45666
diff changeset
   153
    (ctxt
ed5080c03165 some attempts to unify/simplify pretty_goal;
wenzelm
parents: 45666
diff changeset
   154
      |> Config.put show_main_goal main
ed5080c03165 some attempts to unify/simplify pretty_goal;
wenzelm
parents: 45666
diff changeset
   155
      |> not limit ? Config.put goals_limit (Thm.nprems_of th)
ed5080c03165 some attempts to unify/simplify pretty_goal;
wenzelm
parents: 45666
diff changeset
   156
      |> Config.put goals_total false) th);
ed5080c03165 some attempts to unify/simplify pretty_goal;
wenzelm
parents: 45666
diff changeset
   157
32089
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
   158
end;
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
   159
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
   160
end;
568a23753e3a moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff changeset
   161