author | wenzelm |
Thu, 13 Aug 2015 11:05:19 +0200 | |
changeset 60924 | 610794dff23c |
parent 60652 | 65911ba3da23 |
child 61039 | 80f40d89dab6 |
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 |
|
17447 | 54 |
val th = Thm.strip_shyps raw_th; |
28316
b17d863a050f
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset
|
55 |
val {hyps, tpairs, prop, ...} = Thm.rep_thm th; |
55633 | 56 |
val hyps' = if show_hyps then hyps else Thm.undeclared_hyps (Context.Proof ctxt) th; |
57 |
val extra_shyps = Thm.extra_shyps th; |
|
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
20629
diff
changeset
|
58 |
val tags = Thm.get_tags th; |
6087 | 59 |
|
13658
c9ad3e64ddcf
Changed handling of flex-flex constraints: now stored in separate
berghofe
parents:
12831
diff
changeset
|
60 |
val q = if quote then Pretty.quote else I; |
32145
220c9e439d39
clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents:
32090
diff
changeset
|
61 |
val prt_term = q o Syntax.pretty_term ctxt; |
6279 | 62 |
|
28802
9ba30eeec7ce
pretty_thm: oracle flag is always false for now (would require detailed check wrt. promises);
wenzelm
parents:
28316
diff
changeset
|
63 |
|
55633 | 64 |
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
|
65 |
val hsymbs = |
50126
3dec88149176
theorem status about oracles/futures is no longer printed by default;
wenzelm
parents:
49560
diff
changeset
|
66 |
if hlen = 0 then [] |
39166
19efc2af3e6c
turned show_hyps and show_tags into proper configuration option;
wenzelm
parents:
39125
diff
changeset
|
67 |
else if show_hyps orelse show_hyps' then |
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
68 |
[Pretty.brk 2, Pretty.list "[" "]" |
32187 | 69 |
(map (q o Goal_Display.pretty_flexpair ctxt) tpairs @ map prt_term hyps' @ |
55633 | 70 |
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
|
71 |
else [Pretty.brk 2, Pretty.str ("[" ^ replicate_string hlen "." ^ "]")]; |
6087 | 72 |
val tsymbs = |
39166
19efc2af3e6c
turned show_hyps and show_tags into proper configuration option;
wenzelm
parents:
39125
diff
changeset
|
73 |
if null tags orelse not show_tags then [] |
6087 | 74 |
else [Pretty.brk 1, pretty_tags tags]; |
6279 | 75 |
in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end; |
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
76 |
|
50126
3dec88149176
theorem status about oracles/futures is no longer printed by default;
wenzelm
parents:
49560
diff
changeset
|
77 |
fun pretty_thm ctxt = pretty_thm_raw ctxt {quote = false, show_hyps = true}; |
51584 | 78 |
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
|
79 |
|
32145
220c9e439d39
clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents:
32090
diff
changeset
|
80 |
fun pretty_thm_global thy = |
50126
3dec88149176
theorem status about oracles/futures is no longer printed by default;
wenzelm
parents:
49560
diff
changeset
|
81 |
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
|
82 |
|
39acf19e9f3a
moved ProofContext.pretty_thm to Display.pretty_thm etc.;
wenzelm
parents:
32089
diff
changeset
|
83 |
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
|
84 |
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
|
85 |
|
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
86 |
|
4250 | 87 |
|
88 |
(** print theory **) |
|
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
89 |
|
11883 | 90 |
(* pretty_full_theory *) |
4250 | 91 |
|
20629
8f6cc81ba4a3
pretty_full_theory: suppress internal entities by default;
wenzelm
parents:
20226
diff
changeset
|
92 |
fun pretty_full_theory verbose thy = |
4250 | 93 |
let |
35199
2e37cdae7b9c
pretty_full_theory: proper Syntax.init_pretty_global;
wenzelm
parents:
33173
diff
changeset
|
94 |
val ctxt = Syntax.init_pretty_global thy; |
24920 | 95 |
|
96 |
fun prt_cls c = Syntax.pretty_sort ctxt [c]; |
|
97 |
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
|
98 |
fun prt_arity t (c, Ss) = Syntax.pretty_arity ctxt (t, Ss, [c]); |
24920 | 99 |
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
|
100 |
val prt_typ_no_tvars = prt_typ o Logic.unvarifyT_global; |
24920 | 101 |
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
|
102 |
val prt_term_no_vars = prt_term o Logic.unvarify_global; |
50301 | 103 |
fun prt_const (c, ty) = [Pretty.mark_str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty]; |
42384 | 104 |
val prt_const' = Defs.pretty_const ctxt; |
4250 | 105 |
|
14794 | 106 |
fun pretty_classrel (c, []) = prt_cls c |
107 |
| pretty_classrel (c, cs) = Pretty.block |
|
51510
b4f7e6734acc
tuned print_classes: more standard order, markup, formatting;
wenzelm
parents:
51509
diff
changeset
|
108 |
(prt_cls c :: Pretty.str " <" :: Pretty.brk 1 :: Pretty.commas (map prt_cls cs)); |
4250 | 109 |
|
110 |
fun pretty_default S = Pretty.block |
|
14794 | 111 |
[Pretty.str "default sort:", Pretty.brk 1, prt_sort S]; |
4250 | 112 |
|
14996 | 113 |
val tfrees = map (fn v => TFree (v, [])); |
33173
b8ca12f6681a
eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
wenzelm
parents:
33158
diff
changeset
|
114 |
fun pretty_type syn (t, (Type.LogicalType n)) = |
15531 | 115 |
if syn then NONE |
43329
84472e198515
tuned signature: Name.invent and Name.invent_names;
wenzelm
parents:
42384
diff
changeset
|
116 |
else SOME (prt_typ (Type (t, tfrees (Name.invent Name.context Name.aT n)))) |
33173
b8ca12f6681a
eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
wenzelm
parents:
33158
diff
changeset
|
117 |
| pretty_type syn (t, (Type.Abbreviation (vs, U, syn'))) = |
15531 | 118 |
if syn <> syn' then NONE |
119 |
else SOME (Pretty.block |
|
14996 | 120 |
[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
|
121 |
| pretty_type syn (t, Type.Nonterminal) = |
15531 | 122 |
if not syn then NONE |
123 |
else SOME (prt_typ (Type (t, []))); |
|
4250 | 124 |
|
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19420
diff
changeset
|
125 |
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
|
126 |
|
19698 | 127 |
fun pretty_abbrev (c, (ty, t)) = Pretty.block |
128 |
(prt_const (c, ty) @ [Pretty.str " ==", Pretty.brk 1, prt_term_no_vars t]); |
|
129 |
||
50301 | 130 |
fun pretty_axm (a, t) = |
131 |
Pretty.block [Pretty.mark_str a, Pretty.str ":", Pretty.brk 1, prt_term_no_vars t]; |
|
19365 | 132 |
|
19702 | 133 |
fun pretty_finals reds = Pretty.block |
19703 | 134 |
(Pretty.str "final:" :: Pretty.brk 1 :: Pretty.commas (map (prt_const' o fst) reds)); |
19702 | 135 |
|
19698 | 136 |
fun pretty_reduct (lhs, rhs) = Pretty.block |
19702 | 137 |
([prt_const' lhs, Pretty.str " ->", Pretty.brk 2] @ |
60924
610794dff23c
tuned signature, in accordance to sortBy in Scala;
wenzelm
parents:
60652
diff
changeset
|
138 |
Pretty.commas (map prt_const' (sort_by #1 rhs))); |
4250 | 139 |
|
19698 | 140 |
fun pretty_restrict (const, name) = |
141 |
Pretty.block ([prt_const' const, Pretty.brk 2, Pretty.str ("(from " ^ quote name ^ ")")]); |
|
8720 | 142 |
|
24665 | 143 |
val defs = Theory.defs_of thy; |
19698 | 144 |
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
|
145 |
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
|
146 |
val consts = Sign.consts_of thy; |
56025 | 147 |
val {const_space, constants, constraints} = Consts.dest consts; |
148 |
val extern_const = Name_Space.extern ctxt const_space; |
|
26637 | 149 |
val {classes, default, types, ...} = Type.rep_tsig tsig; |
19698 | 150 |
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
|
151 |
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
|
152 |
val arities = Sorts.arities_of class_algebra; |
14996 | 153 |
|
49560 | 154 |
val clsses = |
59917
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
56438
diff
changeset
|
155 |
Name_Space.extern_entries verbose ctxt class_space |
56052 | 156 |
(map (fn ((c, _), cs) => (c, Sign.minimize_sort thy cs)) (Graph.dest classes)) |
56025 | 157 |
|> map (apfst #1); |
59917
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
56438
diff
changeset
|
158 |
val tdecls = Name_Space.extern_table verbose ctxt types |> map (apfst #1); |
56052 | 159 |
val arties = |
59917
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
56438
diff
changeset
|
160 |
Name_Space.extern_entries verbose ctxt (Type.type_space tsig) (Symtab.dest arities) |
56052 | 161 |
|> map (apfst #1); |
20629
8f6cc81ba4a3
pretty_full_theory: suppress internal entities by default;
wenzelm
parents:
20226
diff
changeset
|
162 |
|
59917
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
56438
diff
changeset
|
163 |
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
|
164 |
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
|
165 |
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
|
166 |
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
|
167 |
|
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
56438
diff
changeset
|
168 |
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
|
169 |
|
33158 | 170 |
fun prune_const c = not verbose andalso Consts.is_concealed consts c; |
24774
bc31c318e673
print_theory: observe Markup.internal_property of consts, discontinued special treatment of internal names elsewhere;
wenzelm
parents:
24665
diff
changeset
|
171 |
val (reds0, (reds1, reds2)) = filter_out (prune_const o fst o fst) reducts |
bc31c318e673
print_theory: observe Markup.internal_property of consts, discontinued special treatment of internal names elsewhere;
wenzelm
parents:
24665
diff
changeset
|
172 |
|> map (fn (lhs, rhs) => |
bc31c318e673
print_theory: observe Markup.internal_property of consts, discontinued special treatment of internal names elsewhere;
wenzelm
parents:
24665
diff
changeset
|
173 |
(apfst extern_const lhs, map (apfst extern_const) (filter_out (prune_const o fst) rhs))) |
60924
610794dff23c
tuned signature, in accordance to sortBy in Scala;
wenzelm
parents:
60652
diff
changeset
|
174 |
|> sort_by (#1 o #1) |
19702 | 175 |
|> List.partition (null o #2) |
176 |
||> List.partition (Defs.plain_args o #2 o #1); |
|
60924
610794dff23c
tuned signature, in accordance to sortBy in Scala;
wenzelm
parents:
60652
diff
changeset
|
177 |
val rests = restricts |> map (apfst (apfst extern_const)) |> sort_by (#1 o #1); |
4250 | 178 |
in |
29091 | 179 |
[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
|
180 |
[Pretty.big_list "classes:" (map pretty_classrel clsses), |
8720 | 181 |
pretty_default default, |
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19420
diff
changeset
|
182 |
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
|
183 |
Pretty.big_list "logical types:" (map_filter (pretty_type false) tdecls), |
16534 | 184 |
Pretty.big_list "type arities:" (pretty_arities arties), |
19698 | 185 |
Pretty.big_list "logical consts:" (map (Pretty.block o prt_const) log_cnsts), |
19365 | 186 |
Pretty.big_list "abbreviations:" (map pretty_abbrev abbrevs), |
19698 | 187 |
Pretty.big_list "constraints:" (map (Pretty.block o prt_const) cnstrs), |
188 |
Pretty.big_list "axioms:" (map pretty_axm axms), |
|
50301 | 189 |
Pretty.block |
59917
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
56438
diff
changeset
|
190 |
(Pretty.breaks (Pretty.str "oracles:" :: |
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
56438
diff
changeset
|
191 |
map Pretty.mark_str (Thm.extern_oracles verbose ctxt))), |
19698 | 192 |
Pretty.big_list "definitions:" |
19702 | 193 |
[pretty_finals reds0, |
194 |
Pretty.big_list "non-overloaded:" (map pretty_reduct reds1), |
|
195 |
Pretty.big_list "overloaded:" (map pretty_reduct reds2), |
|
196 |
Pretty.big_list "pattern restrictions:" (map pretty_restrict rests)]] |
|
4250 | 197 |
end; |
198 |
||
1591
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
199 |
end; |
7fa0265dcd13
New module for display/printing operations, taken from drule.ML
paulson
parents:
diff
changeset
|
200 |
|
32089
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
30723
diff
changeset
|
201 |
structure Basic_Display: BASIC_DISPLAY = Display; |
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
30723
diff
changeset
|
202 |
open Basic_Display; |