author | wenzelm |
Tue, 22 Sep 2015 18:06:49 +0200 | |
changeset 61251 | 2da25a27a616 |
parent 61249 | 8611f408ec13 |
child 61252 | c165f0472d57 |
permissions | -rw-r--r-- |
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
1 |
(* Title: Pure/display.ML |
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
32089
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
30723
diff
changeset
|
3 |
Author: Makarius |
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
4 |
|
32089
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
30723
diff
changeset
|
5 |
Printing of theorems, results etc. |
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
6 |
*) |
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
7 |
|
11883 | 8 |
signature BASIC_DISPLAY = |
9 |
sig |
|
39050
600de0485859
turned show_consts into proper configuration option;
wenzelm
parents:
37248
diff
changeset
|
10 |
val show_consts: bool Config.T |
39166
19efc2af3e6c
turned show_hyps and show_tags into proper configuration option;
wenzelm
parents:
39125
diff
changeset
|
11 |
val show_hyps_raw: Config.raw |
19efc2af3e6c
turned show_hyps and show_tags into proper configuration option;
wenzelm
parents:
39125
diff
changeset
|
12 |
val show_hyps: bool Config.T |
19efc2af3e6c
turned show_hyps and show_tags into proper configuration option;
wenzelm
parents:
39125
diff
changeset
|
13 |
val show_tags_raw: Config.raw |
19efc2af3e6c
turned show_hyps and show_tags into proper configuration option;
wenzelm
parents:
39125
diff
changeset
|
14 |
val show_tags: bool Config.T |
11883 | 15 |
end; |
16 |
||
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
17 |
signature DISPLAY = |
4950 | 18 |
sig |
11883 | 19 |
include BASIC_DISPLAY |
50126
3dec88149176
theorem status about oracles/futures is no longer printed by default;
wenzelm
parents:
49560
diff
changeset
|
20 |
val pretty_thm_raw: Proof.context -> {quote: bool, show_hyps: bool} -> thm -> Pretty.T |
32090
39acf19e9f3a
moved ProofContext.pretty_thm to Display.pretty_thm etc.;
wenzelm
parents:
32089
diff
changeset
|
21 |
val pretty_thm: Proof.context -> thm -> Pretty.T |
51584 | 22 |
val pretty_thm_item: Proof.context -> thm -> Pretty.T |
32090
39acf19e9f3a
moved ProofContext.pretty_thm to Display.pretty_thm etc.;
wenzelm
parents:
32089
diff
changeset
|
23 |
val pretty_thm_global: theory -> thm -> Pretty.T |
39acf19e9f3a
moved ProofContext.pretty_thm to Display.pretty_thm etc.;
wenzelm
parents:
32089
diff
changeset
|
24 |
val string_of_thm: Proof.context -> thm -> string |
39acf19e9f3a
moved ProofContext.pretty_thm to Display.pretty_thm etc.;
wenzelm
parents:
32089
diff
changeset
|
25 |
val string_of_thm_global: theory -> thm -> string |
20629
8f6cc81ba4a3
pretty_full_theory: suppress internal entities by default;
wenzelm
parents:
20226
diff
changeset
|
26 |
val pretty_full_theory: bool -> theory -> Pretty.T list |
4950 | 27 |
end; |
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
28 |
|
4950 | 29 |
structure Display: DISPLAY = |
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
30 |
struct |
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
31 |
|
32089
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
30723
diff
changeset
|
32 |
(** options **) |
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
30723
diff
changeset
|
33 |
|
32187 | 34 |
val show_consts = Goal_Display.show_consts; |
32089
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
30723
diff
changeset
|
35 |
|
56438 | 36 |
val show_hyps_raw = Config.declare ("show_hyps", @{here}) (fn _ => Config.Bool false); |
39166
19efc2af3e6c
turned show_hyps and show_tags into proper configuration option;
wenzelm
parents:
39125
diff
changeset
|
37 |
val show_hyps = Config.bool show_hyps_raw; |
19efc2af3e6c
turned show_hyps and show_tags into proper configuration option;
wenzelm
parents:
39125
diff
changeset
|
38 |
|
56438 | 39 |
val show_tags_raw = Config.declare ("show_tags", @{here}) (fn _ => Config.Bool false); |
39166
19efc2af3e6c
turned show_hyps and show_tags into proper configuration option;
wenzelm
parents:
39125
diff
changeset
|
40 |
val show_tags = Config.bool show_tags_raw; |
32089
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
30723
diff
changeset
|
41 |
|
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
30723
diff
changeset
|
42 |
|
11883 | 43 |
|
6087 | 44 |
(** print thm **) |
45 |
||
28840 | 46 |
fun pretty_tag (name, arg) = Pretty.strs [name, quote arg]; |
6087 | 47 |
val pretty_tags = Pretty.list "[" "]" o map pretty_tag; |
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
48 |
|
50126
3dec88149176
theorem status about oracles/futures is no longer printed by default;
wenzelm
parents:
49560
diff
changeset
|
49 |
fun pretty_thm_raw ctxt {quote, show_hyps = show_hyps'} raw_th = |
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
50 |
let |
39166
19efc2af3e6c
turned show_hyps and show_tags into proper configuration option;
wenzelm
parents:
39125
diff
changeset
|
51 |
val show_tags = Config.get ctxt show_tags; |
19efc2af3e6c
turned show_hyps and show_tags into proper configuration option;
wenzelm
parents:
39125
diff
changeset
|
52 |
val show_hyps = Config.get ctxt show_hyps; |
19efc2af3e6c
turned show_hyps and show_tags into proper configuration option;
wenzelm
parents:
39125
diff
changeset
|
53 |
|
61052 | 54 |
val th = raw_th |
55 |
|> perhaps (try (Thm.transfer (Proof_Context.theory_of ctxt))) |
|
56 |
|> perhaps (try Thm.strip_shyps); |
|
61039 | 57 |
|
58 |
val hyps = if show_hyps then Thm.hyps_of th else Thm.undeclared_hyps (Context.Proof ctxt) th; |
|
55633 | 59 |
val extra_shyps = Thm.extra_shyps th; |
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
20629
diff
changeset
|
60 |
val tags = Thm.get_tags th; |
61039 | 61 |
val tpairs = Thm.tpairs_of th; |
6087 | 62 |
|
13658
c9ad3e64ddcf
Changed handling of flex-flex constraints: now stored in separate
berghofe
parents:
12831
diff
changeset
|
63 |
val q = if quote then Pretty.quote else I; |
32145
220c9e439d39
clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents:
32090
diff
changeset
|
64 |
val prt_term = q o Syntax.pretty_term ctxt; |
6279 | 65 |
|
28802
9ba30eeec7ce
pretty_thm: oracle flag is always false for now (would require detailed check wrt. promises);
wenzelm
parents:
28316
diff
changeset
|
66 |
|
61039 | 67 |
val hlen = length extra_shyps + length hyps + length tpairs; |
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
68 |
val hsymbs = |
50126
3dec88149176
theorem status about oracles/futures is no longer printed by default;
wenzelm
parents:
49560
diff
changeset
|
69 |
if hlen = 0 then [] |
39166
19efc2af3e6c
turned show_hyps and show_tags into proper configuration option;
wenzelm
parents:
39125
diff
changeset
|
70 |
else if show_hyps orelse show_hyps' then |
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
71 |
[Pretty.brk 2, Pretty.list "[" "]" |
61039 | 72 |
(map (q o Goal_Display.pretty_flexpair ctxt) tpairs @ map prt_term hyps @ |
55633 | 73 |
map (Syntax.pretty_sort ctxt) extra_shyps)] |
50126
3dec88149176
theorem status about oracles/futures is no longer printed by default;
wenzelm
parents:
49560
diff
changeset
|
74 |
else [Pretty.brk 2, Pretty.str ("[" ^ replicate_string hlen "." ^ "]")]; |
6087 | 75 |
val tsymbs = |
39166
19efc2af3e6c
turned show_hyps and show_tags into proper configuration option;
wenzelm
parents:
39125
diff
changeset
|
76 |
if null tags orelse not show_tags then [] |
6087 | 77 |
else [Pretty.brk 1, pretty_tags tags]; |
61039 | 78 |
in Pretty.block (prt_term (Thm.prop_of th) :: (hsymbs @ tsymbs)) end; |
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
79 |
|
50126
3dec88149176
theorem status about oracles/futures is no longer printed by default;
wenzelm
parents:
49560
diff
changeset
|
80 |
fun pretty_thm ctxt = pretty_thm_raw ctxt {quote = false, show_hyps = true}; |
51584 | 81 |
fun pretty_thm_item ctxt th = Pretty.item [pretty_thm ctxt th]; |
32090
39acf19e9f3a
moved ProofContext.pretty_thm to Display.pretty_thm etc.;
wenzelm
parents:
32089
diff
changeset
|
82 |
|
32145
220c9e439d39
clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents:
32090
diff
changeset
|
83 |
fun pretty_thm_global thy = |
50126
3dec88149176
theorem status about oracles/futures is no longer printed by default;
wenzelm
parents:
49560
diff
changeset
|
84 |
pretty_thm_raw (Syntax.init_pretty_global thy) {quote = false, show_hyps = false}; |
32090
39acf19e9f3a
moved ProofContext.pretty_thm to Display.pretty_thm etc.;
wenzelm
parents:
32089
diff
changeset
|
85 |
|
39acf19e9f3a
moved ProofContext.pretty_thm to Display.pretty_thm etc.;
wenzelm
parents:
32089
diff
changeset
|
86 |
val string_of_thm = Pretty.string_of oo pretty_thm; |
39acf19e9f3a
moved ProofContext.pretty_thm to Display.pretty_thm etc.;
wenzelm
parents:
32089
diff
changeset
|
87 |
val string_of_thm_global = Pretty.string_of oo pretty_thm_global; |
39acf19e9f3a
moved ProofContext.pretty_thm to Display.pretty_thm etc.;
wenzelm
parents:
32089
diff
changeset
|
88 |
|
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
89 |
|
4250 | 90 |
|
91 |
(** print theory **) |
|
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
92 |
|
11883 | 93 |
(* pretty_full_theory *) |
4250 | 94 |
|
20629
8f6cc81ba4a3
pretty_full_theory: suppress internal entities by default;
wenzelm
parents:
20226
diff
changeset
|
95 |
fun pretty_full_theory verbose thy = |
4250 | 96 |
let |
35199
2e37cdae7b9c
pretty_full_theory: proper Syntax.init_pretty_global;
wenzelm
parents:
33173
diff
changeset
|
97 |
val ctxt = Syntax.init_pretty_global thy; |
24920 | 98 |
|
99 |
fun prt_cls c = Syntax.pretty_sort ctxt [c]; |
|
100 |
fun prt_sort S = Syntax.pretty_sort ctxt S; |
|
37248
8e8e5f9d1441
arities: no need to maintain original codomain (cf. f795c1164708) -- completion happens in axclass.ML;
wenzelm
parents:
36328
diff
changeset
|
101 |
fun prt_arity t (c, Ss) = Syntax.pretty_arity ctxt (t, Ss, [c]); |
24920 | 102 |
fun prt_typ ty = Pretty.quote (Syntax.pretty_typ ctxt ty); |
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35199
diff
changeset
|
103 |
val prt_typ_no_tvars = prt_typ o Logic.unvarifyT_global; |
24920 | 104 |
fun prt_term t = Pretty.quote (Syntax.pretty_term ctxt t); |
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35199
diff
changeset
|
105 |
val prt_term_no_vars = prt_term o Logic.unvarify_global; |
50301 | 106 |
fun prt_const (c, ty) = [Pretty.mark_str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty]; |
61249 | 107 |
val prt_item = Defs.pretty_item ctxt; |
108 |
fun sort_item_by f = sort (Defs.item_ord o apply2 f); |
|
4250 | 109 |
|
14794 | 110 |
fun pretty_classrel (c, []) = prt_cls c |
111 |
| pretty_classrel (c, cs) = Pretty.block |
|
51510
b4f7e6734acc
tuned print_classes: more standard order, markup, formatting;
wenzelm
parents:
51509
diff
changeset
|
112 |
(prt_cls c :: Pretty.str " <" :: Pretty.brk 1 :: Pretty.commas (map prt_cls cs)); |
4250 | 113 |
|
114 |
fun pretty_default S = Pretty.block |
|
14794 | 115 |
[Pretty.str "default sort:", Pretty.brk 1, prt_sort S]; |
4250 | 116 |
|
14996 | 117 |
val tfrees = map (fn v => TFree (v, [])); |
61251 | 118 |
fun pretty_type syn (t, Type.LogicalType n) = |
15531 | 119 |
if syn then NONE |
43329
84472e198515
tuned signature: Name.invent and Name.invent_names;
wenzelm
parents:
42384
diff
changeset
|
120 |
else SOME (prt_typ (Type (t, tfrees (Name.invent Name.context Name.aT n)))) |
61251 | 121 |
| pretty_type syn (t, Type.Abbreviation (vs, U, syn')) = |
15531 | 122 |
if syn <> syn' then NONE |
123 |
else SOME (Pretty.block |
|
14996 | 124 |
[prt_typ (Type (t, tfrees vs)), Pretty.str " =", Pretty.brk 1, prt_typ U]) |
33173
b8ca12f6681a
eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
wenzelm
parents:
33158
diff
changeset
|
125 |
| pretty_type syn (t, Type.Nonterminal) = |
15531 | 126 |
if not syn then NONE |
127 |
else SOME (prt_typ (Type (t, []))); |
|
4250 | 128 |
|
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19420
diff
changeset
|
129 |
val pretty_arities = maps (fn (t, ars) => map (prt_arity t) ars); |
14223
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14178
diff
changeset
|
130 |
|
19698 | 131 |
fun pretty_abbrev (c, (ty, t)) = Pretty.block |
132 |
(prt_const (c, ty) @ [Pretty.str " ==", Pretty.brk 1, prt_term_no_vars t]); |
|
133 |
||
50301 | 134 |
fun pretty_axm (a, t) = |
135 |
Pretty.block [Pretty.mark_str a, Pretty.str ":", Pretty.brk 1, prt_term_no_vars t]; |
|
19365 | 136 |
|
19702 | 137 |
fun pretty_finals reds = Pretty.block |
61249 | 138 |
(Pretty.str "final:" :: Pretty.brk 1 :: Pretty.commas (map (prt_item o fst) reds)); |
19702 | 139 |
|
19698 | 140 |
fun pretty_reduct (lhs, rhs) = Pretty.block |
61249 | 141 |
([prt_item lhs, Pretty.str " ->", Pretty.brk 2] @ |
142 |
Pretty.commas (map prt_item (sort_item_by #1 rhs))); |
|
4250 | 143 |
|
19698 | 144 |
fun pretty_restrict (const, name) = |
61249 | 145 |
Pretty.block ([prt_item const, Pretty.brk 2, Pretty.str ("(from " ^ quote name ^ ")")]); |
8720 | 146 |
|
24665 | 147 |
val defs = Theory.defs_of thy; |
19698 | 148 |
val {restricts, reducts} = Defs.dest defs; |
47005
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
43329
diff
changeset
|
149 |
val tsig = Sign.tsig_of thy; |
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
43329
diff
changeset
|
150 |
val consts = Sign.consts_of thy; |
56025 | 151 |
val {const_space, constants, constraints} = Consts.dest consts; |
26637 | 152 |
val {classes, default, types, ...} = Type.rep_tsig tsig; |
61246
077b88f9ec16
HOL typedef with explicit dependency checks according to Ondrey Kuncar, 07-Jul-2015, 16-Jul-2015, 30-Jul-2015;
wenzelm
parents:
61052
diff
changeset
|
153 |
val type_space = Type.type_space tsig; |
19698 | 154 |
val (class_space, class_algebra) = classes; |
36328
4d9deabf6474
replaced Sorts.rep_algebra by slightly more abstract selectors classes_of/arities_of;
wenzelm
parents:
35845
diff
changeset
|
155 |
val classes = Sorts.classes_of class_algebra; |
4d9deabf6474
replaced Sorts.rep_algebra by slightly more abstract selectors classes_of/arities_of;
wenzelm
parents:
35845
diff
changeset
|
156 |
val arities = Sorts.arities_of class_algebra; |
14996 | 157 |
|
61251 | 158 |
val item_space = fn Defs.Constant => const_space | Defs.Type => type_space; |
159 |
fun extern_item (k, c) = (k, Name_Space.extern ctxt (item_space k) c); |
|
160 |
fun prune_item (k, c) = not verbose andalso Name_Space.is_concealed (item_space k) c; |
|
61246
077b88f9ec16
HOL typedef with explicit dependency checks according to Ondrey Kuncar, 07-Jul-2015, 16-Jul-2015, 30-Jul-2015;
wenzelm
parents:
61052
diff
changeset
|
161 |
|
49560 | 162 |
val clsses = |
59917
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
56438
diff
changeset
|
163 |
Name_Space.extern_entries verbose ctxt class_space |
56052 | 164 |
(map (fn ((c, _), cs) => (c, Sign.minimize_sort thy cs)) (Graph.dest classes)) |
56025 | 165 |
|> map (apfst #1); |
59917
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
56438
diff
changeset
|
166 |
val tdecls = Name_Space.extern_table verbose ctxt types |> map (apfst #1); |
56052 | 167 |
val arties = |
61251 | 168 |
Name_Space.extern_entries verbose ctxt type_space (Symtab.dest arities) |
56052 | 169 |
|> map (apfst #1); |
20629
8f6cc81ba4a3
pretty_full_theory: suppress internal entities by default;
wenzelm
parents:
20226
diff
changeset
|
170 |
|
59917
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
56438
diff
changeset
|
171 |
val cnsts = Name_Space.markup_entries verbose ctxt const_space constants; |
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
56438
diff
changeset
|
172 |
val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts; |
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
56438
diff
changeset
|
173 |
val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts; |
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
56438
diff
changeset
|
174 |
val cnstrs = Name_Space.markup_entries verbose ctxt const_space constraints; |
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
56438
diff
changeset
|
175 |
|
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
56438
diff
changeset
|
176 |
val axms = Name_Space.markup_table verbose ctxt (Theory.axiom_table thy); |
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
56438
diff
changeset
|
177 |
|
61249 | 178 |
val (reds0, (reds1, reds2)) = filter_out (prune_item o fst o fst) reducts |
24774
bc31c318e673
print_theory: observe Markup.internal_property of consts, discontinued special treatment of internal names elsewhere;
wenzelm
parents:
24665
diff
changeset
|
179 |
|> map (fn (lhs, rhs) => |
61249 | 180 |
(apfst extern_item lhs, map (apfst extern_item) (filter_out (prune_item o fst) rhs))) |
181 |
|> sort_item_by (#1 o #1) |
|
19702 | 182 |
|> List.partition (null o #2) |
183 |
||> List.partition (Defs.plain_args o #2 o #1); |
|
61249 | 184 |
val rests = restricts |> map (apfst (apfst extern_item)) |> sort_item_by (#1 o #1); |
4250 | 185 |
in |
29091 | 186 |
[Pretty.strs ("names:" :: Context.display_names thy)] @ |
30409
6037cac149a1
pretty_full_theory: no longer display name prefix -- naming is far more complex now;
wenzelm
parents:
30186
diff
changeset
|
187 |
[Pretty.big_list "classes:" (map pretty_classrel clsses), |
8720 | 188 |
pretty_default default, |
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19420
diff
changeset
|
189 |
Pretty.big_list "syntactic types:" (map_filter (pretty_type true) tdecls), |
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19420
diff
changeset
|
190 |
Pretty.big_list "logical types:" (map_filter (pretty_type false) tdecls), |
16534 | 191 |
Pretty.big_list "type arities:" (pretty_arities arties), |
19698 | 192 |
Pretty.big_list "logical consts:" (map (Pretty.block o prt_const) log_cnsts), |
19365 | 193 |
Pretty.big_list "abbreviations:" (map pretty_abbrev abbrevs), |
19698 | 194 |
Pretty.big_list "constraints:" (map (Pretty.block o prt_const) cnstrs), |
195 |
Pretty.big_list "axioms:" (map pretty_axm axms), |
|
50301 | 196 |
Pretty.block |
59917
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
56438
diff
changeset
|
197 |
(Pretty.breaks (Pretty.str "oracles:" :: |
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
56438
diff
changeset
|
198 |
map Pretty.mark_str (Thm.extern_oracles verbose ctxt))), |
19698 | 199 |
Pretty.big_list "definitions:" |
19702 | 200 |
[pretty_finals reds0, |
201 |
Pretty.big_list "non-overloaded:" (map pretty_reduct reds1), |
|
202 |
Pretty.big_list "overloaded:" (map pretty_reduct reds2), |
|
203 |
Pretty.big_list "pattern restrictions:" (map pretty_restrict rests)]] |
|
4250 | 204 |
end; |
205 |
||
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
206 |
end; |
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
207 |
|
32089
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
30723
diff
changeset
|
208 |
structure Basic_Display: BASIC_DISPLAY = Display; |
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
30723
diff
changeset
|
209 |
open Basic_Display; |