author | blanchet |
Thu, 16 Dec 2010 22:45:02 +0100 | |
changeset 41220 | 4d11b0de7dd8 |
parent 39163 | 4d701c0388c3 |
child 45666 | d83797ef0d2d |
permissions | -rw-r--r-- |
32187 | 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 | 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 |
32089
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset
|
23 |
end; |
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset
|
24 |
|
32187 | 25 |
structure Goal_Display: GOAL_DISPLAY = |
32089
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset
|
26 |
struct |
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset
|
27 |
|
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
|
28 |
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
|
29 |
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
|
30 |
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
|
31 |
|
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 |
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
|
33 |
|
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
|
34 |
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
|
35 |
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
|
36 |
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
|
37 |
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
|
38 |
|
39050
600de0485859
turned show_consts into proper configuration option;
wenzelm
parents:
33957
diff
changeset
|
39 |
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
|
40 |
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
|
41 |
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
|
42 |
|
32145
220c9e439d39
clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents:
32089
diff
changeset
|
43 |
fun pretty_flexpair ctxt (t, u) = Pretty.block |
220c9e439d39
clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents:
32089
diff
changeset
|
44 |
[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
|
45 |
|
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 |
(*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
|
48 |
|
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset
|
49 |
local |
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset
|
50 |
|
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset
|
51 |
fun ins_entry (x, y) = |
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset
|
52 |
AList.default (op =) (x, []) #> |
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset
|
53 |
AList.map_entry (op =) x (insert (op =) y); |
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset
|
54 |
|
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset
|
55 |
val add_consts = Term.fold_aterms |
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset
|
56 |
(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
|
57 |
| _ => I); |
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset
|
58 |
|
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset
|
59 |
val add_vars = Term.fold_aterms |
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset
|
60 |
(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
|
61 |
| Var (xi, T) => ins_entry (T, xi) |
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset
|
62 |
| _ => I); |
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset
|
63 |
|
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset
|
64 |
val add_varsT = Term.fold_atyps |
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset
|
65 |
(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
|
66 |
| TVar (xi, S) => ins_entry (S, xi) |
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset
|
67 |
| _ => I); |
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset
|
68 |
|
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset
|
69 |
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
|
70 |
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
|
71 |
|
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset
|
72 |
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
|
73 |
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
|
74 |
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
|
75 |
|
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset
|
76 |
in |
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset
|
77 |
|
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
|
78 |
fun pretty_goals ctxt0 state = |
32089
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset
|
79 |
let |
39134
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39125
diff
changeset
|
80 |
val ctxt = ctxt0 |
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39125
diff
changeset
|
81 |
|> Config.put show_free_types false |
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39125
diff
changeset
|
82 |
|> Config.put show_types |
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39125
diff
changeset
|
83 |
(Config.get ctxt0 show_types orelse |
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39125
diff
changeset
|
84 |
Config.get ctxt0 show_sorts orelse |
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39125
diff
changeset
|
85 |
Config.get ctxt0 show_all_types) |
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39125
diff
changeset
|
86 |
|> 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
|
87 |
|
39134
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39125
diff
changeset
|
88 |
val show_sorts0 = Config.get ctxt0 show_sorts; |
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39125
diff
changeset
|
89 |
val show_types = Config.get ctxt show_types; |
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39125
diff
changeset
|
90 |
val show_consts = Config.get ctxt show_consts |
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39125
diff
changeset
|
91 |
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
|
92 |
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
|
93 |
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
|
94 |
|
32145
220c9e439d39
clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents:
32089
diff
changeset
|
95 |
val prt_sort = Syntax.pretty_sort ctxt; |
220c9e439d39
clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents:
32089
diff
changeset
|
96 |
val prt_typ = Syntax.pretty_typ ctxt; |
220c9e439d39
clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents:
32089
diff
changeset
|
97 |
val prt_term = Syntax.pretty_term ctxt; |
220c9e439d39
clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents:
32089
diff
changeset
|
98 |
|
32089
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset
|
99 |
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
|
100 |
[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
|
101 |
Pretty.brk 1, prtT X]; |
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset
|
102 |
|
32145
220c9e439d39
clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents:
32089
diff
changeset
|
103 |
fun prt_var (x, ~1) = prt_term (Syntax.free x) |
220c9e439d39
clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents:
32089
diff
changeset
|
104 |
| 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
|
105 |
|
32145
220c9e439d39
clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents:
32089
diff
changeset
|
106 |
fun prt_varT (x, ~1) = prt_typ (TFree (x, [])) |
220c9e439d39
clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents:
32089
diff
changeset
|
107 |
| prt_varT xi = prt_typ (TVar (xi, [])); |
32089
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset
|
108 |
|
32145
220c9e439d39
clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents:
32089
diff
changeset
|
109 |
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
|
110 |
val prt_vars = prt_atoms prt_var prt_typ; |
220c9e439d39
clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents:
32089
diff
changeset
|
111 |
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
|
112 |
|
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 |
fun pretty_list _ _ [] = [] |
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset
|
115 |
| 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
|
116 |
|
32167
d32817dda0e6
Display_Goal.pretty_goals: always Markup.subgoal, clarified options;
wenzelm
parents:
32145
diff
changeset
|
117 |
fun pretty_subgoal (n, A) = Pretty.markup Markup.subgoal |
32145
220c9e439d39
clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents:
32089
diff
changeset
|
118 |
[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
|
119 |
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
|
120 |
|
32145
220c9e439d39
clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents:
32089
diff
changeset
|
121 |
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
|
122 |
|
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset
|
123 |
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
|
124 |
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
|
125 |
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
|
126 |
|
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 |
val {prop, tpairs, ...} = Thm.rep_thm state; |
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset
|
129 |
val (As, B) = Logic.strip_horn prop; |
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset
|
130 |
val ngoals = length As; |
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset
|
131 |
in |
39134
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39125
diff
changeset
|
132 |
(if show_main_goal then [prt_term B] else []) @ |
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39125
diff
changeset
|
133 |
(if ngoals = 0 then [Pretty.str "No subgoals!"] |
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39125
diff
changeset
|
134 |
else if ngoals > goals_limit then |
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39125
diff
changeset
|
135 |
pretty_subgoals (take goals_limit As) @ |
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39125
diff
changeset
|
136 |
(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
|
137 |
else []) |
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39125
diff
changeset
|
138 |
else pretty_subgoals As) @ |
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39125
diff
changeset
|
139 |
pretty_ffpairs tpairs @ |
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39125
diff
changeset
|
140 |
(if show_consts then pretty_consts prop else []) @ |
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39125
diff
changeset
|
141 |
(if show_types then pretty_vars prop else []) @ |
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39125
diff
changeset
|
142 |
(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
|
143 |
end; |
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset
|
144 |
|
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
|
145 |
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
|
146 |
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
|
147 |
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
|
148 |
in pretty_goals ctxt th end; |
32089
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset
|
149 |
|
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset
|
150 |
end; |
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset
|
151 |
|
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset
|
152 |
end; |
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset
|
153 |