31 val pretty_flexpair: Pretty.pp -> term * term -> Pretty.T |
31 val pretty_flexpair: Pretty.pp -> term * term -> Pretty.T |
32 val pretty_thm_aux: Pretty.pp -> bool -> thm -> Pretty.T |
32 val pretty_thm_aux: Pretty.pp -> bool -> thm -> Pretty.T |
33 val pretty_thm_no_quote: thm -> Pretty.T |
33 val pretty_thm_no_quote: thm -> Pretty.T |
34 val pretty_thm: thm -> Pretty.T |
34 val pretty_thm: thm -> Pretty.T |
35 val pretty_thms: thm list -> Pretty.T |
35 val pretty_thms: thm list -> Pretty.T |
36 val pretty_thm_sg: Sign.sg -> thm -> Pretty.T |
36 val pretty_thm_sg: theory -> thm -> Pretty.T |
37 val pretty_thms_sg: Sign.sg -> thm list -> Pretty.T |
37 val pretty_thms_sg: theory -> thm list -> Pretty.T |
38 val pprint_thm: thm -> pprint_args -> unit |
38 val pprint_thm: thm -> pprint_args -> unit |
39 val pretty_ctyp: ctyp -> Pretty.T |
39 val pretty_ctyp: ctyp -> Pretty.T |
40 val pprint_ctyp: ctyp -> pprint_args -> unit |
40 val pprint_ctyp: ctyp -> pprint_args -> unit |
41 val pretty_cterm: cterm -> Pretty.T |
41 val pretty_cterm: cterm -> Pretty.T |
42 val pprint_cterm: cterm -> pprint_args -> unit |
42 val pprint_cterm: cterm -> pprint_args -> unit |
43 val pretty_theory: theory -> Pretty.T |
|
44 val pprint_theory: theory -> pprint_args -> unit |
|
45 val pretty_full_theory: theory -> Pretty.T list |
43 val pretty_full_theory: theory -> Pretty.T list |
46 val pretty_name_space: string * NameSpace.T -> Pretty.T |
|
47 val pretty_goals_aux: Pretty.pp -> string -> bool * bool -> int -> thm -> Pretty.T list |
44 val pretty_goals_aux: Pretty.pp -> string -> bool * bool -> int -> thm -> Pretty.T list |
48 val pretty_goals: int -> thm -> Pretty.T list |
45 val pretty_goals: int -> thm -> Pretty.T list |
49 val print_goals: int -> thm -> unit |
46 val print_goals: int -> thm -> unit |
50 val current_goals_markers: (string * string * string) ref |
47 val current_goals_markers: (string * string * string) ref |
51 val pretty_current_goals: int -> int -> thm -> Pretty.T list |
48 val pretty_current_goals: int -> int -> thm -> Pretty.T list |
92 if null tags orelse not (! show_tags) then [] |
89 if null tags orelse not (! show_tags) then [] |
93 else [Pretty.brk 1, pretty_tags tags]; |
90 else [Pretty.brk 1, pretty_tags tags]; |
94 in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end; |
91 in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end; |
95 |
92 |
96 fun gen_pretty_thm quote th = |
93 fun gen_pretty_thm quote th = |
97 pretty_thm_aux (Sign.pp (Thm.sign_of_thm th)) quote th; |
94 pretty_thm_aux (Sign.pp (Thm.theory_of_thm th)) quote th; |
98 |
95 |
99 val pretty_thm = gen_pretty_thm true; |
96 val pretty_thm = gen_pretty_thm true; |
100 val pretty_thm_no_quote = gen_pretty_thm false; |
97 val pretty_thm_no_quote = gen_pretty_thm false; |
101 |
98 |
102 |
99 |
126 |
123 |
127 |
124 |
128 (* other printing commands *) |
125 (* other printing commands *) |
129 |
126 |
130 fun pretty_ctyp cT = |
127 fun pretty_ctyp cT = |
131 let val {sign, T} = rep_ctyp cT in Sign.pretty_typ sign T end; |
128 let val {thy, T, ...} = rep_ctyp cT in Sign.pretty_typ thy T end; |
132 |
129 |
133 fun pprint_ctyp cT = |
130 fun pprint_ctyp cT = |
134 let val {sign, T} = rep_ctyp cT in Sign.pprint_typ sign T end; |
131 let val {thy, T, ...} = rep_ctyp cT in Sign.pprint_typ thy T end; |
135 |
132 |
136 fun string_of_ctyp cT = |
133 fun string_of_ctyp cT = |
137 let val {sign, T} = rep_ctyp cT in Sign.string_of_typ sign T end; |
134 let val {thy, T, ...} = rep_ctyp cT in Sign.string_of_typ thy T end; |
138 |
135 |
139 val print_ctyp = writeln o string_of_ctyp; |
136 val print_ctyp = writeln o string_of_ctyp; |
140 |
137 |
141 fun pretty_cterm ct = |
138 fun pretty_cterm ct = |
142 let val {sign, t, ...} = rep_cterm ct in Sign.pretty_term sign t end; |
139 let val {thy, t, ...} = rep_cterm ct in Sign.pretty_term thy t end; |
143 |
140 |
144 fun pprint_cterm ct = |
141 fun pprint_cterm ct = |
145 let val {sign, t, ...} = rep_cterm ct in Sign.pprint_term sign t end; |
142 let val {thy, t, ...} = rep_cterm ct in Sign.pprint_term thy t end; |
146 |
143 |
147 fun string_of_cterm ct = |
144 fun string_of_cterm ct = |
148 let val {sign, t, ...} = rep_cterm ct in Sign.string_of_term sign t end; |
145 let val {thy, t, ...} = rep_cterm ct in Sign.string_of_term thy t end; |
149 |
146 |
150 val print_cterm = writeln o string_of_cterm; |
147 val print_cterm = writeln o string_of_cterm; |
151 |
148 |
152 |
149 |
153 |
150 |
154 (** print theory **) |
151 (** print theory **) |
155 |
152 |
156 val pretty_theory = Sign.pretty_sg o Theory.sign_of; |
153 val print_syntax = Syntax.print_syntax o Sign.syn_of; |
157 val pprint_theory = Sign.pprint_sg o Theory.sign_of; |
|
158 |
|
159 val print_syntax = Syntax.print_syntax o Theory.syn_of; |
|
160 |
|
161 |
|
162 (* pretty_name_space *) |
|
163 |
|
164 fun pretty_name_space (kind, space) = |
|
165 let |
|
166 fun prt_entry (name, accs) = Pretty.block |
|
167 (Pretty.str (Library.quote name ^ " =") :: Pretty.brk 1 :: |
|
168 Pretty.commas (map (Pretty.quote o Pretty.str) accs)); |
|
169 in |
|
170 Pretty.fbreaks (Pretty.str (kind ^ ":") :: map prt_entry (NameSpace.dest space)) |
|
171 |> Pretty.block |
|
172 end; |
|
173 |
154 |
174 |
155 |
175 (* pretty_full_theory *) |
156 (* pretty_full_theory *) |
176 |
157 |
177 fun pretty_full_theory thy = |
158 fun pretty_full_theory thy = |
178 let |
159 let |
179 val sg = Theory.sign_of thy; |
160 fun prt_cls c = Sign.pretty_sort thy [c]; |
180 |
161 fun prt_sort S = Sign.pretty_sort thy S; |
181 fun prt_cls c = Sign.pretty_sort sg [c]; |
162 fun prt_arity t (c, Ss) = Sign.pretty_arity thy (t, Ss, [c]); |
182 fun prt_sort S = Sign.pretty_sort sg S; |
163 fun prt_typ ty = Pretty.quote (Sign.pretty_typ thy ty); |
183 fun prt_arity t (c, Ss) = Sign.pretty_arity sg (t, Ss, [c]); |
|
184 fun prt_typ ty = Pretty.quote (Sign.pretty_typ sg ty); |
|
185 val prt_typ_no_tvars = prt_typ o Type.freeze_type; |
164 val prt_typ_no_tvars = prt_typ o Type.freeze_type; |
186 fun prt_term t = Pretty.quote (Sign.pretty_term sg t); |
165 fun prt_term t = Pretty.quote (Sign.pretty_term thy t); |
187 |
166 |
188 fun pretty_classrel (c, []) = prt_cls c |
167 fun pretty_classrel (c, []) = prt_cls c |
189 | pretty_classrel (c, cs) = Pretty.block |
168 | pretty_classrel (c, cs) = Pretty.block |
190 (prt_cls c :: Pretty.str " <" :: Pretty.brk 1 :: |
169 (prt_cls c :: Pretty.str " <" :: Pretty.brk 1 :: |
191 Pretty.commas (map prt_cls cs)); |
170 Pretty.commas (map prt_cls cs)); |
220 (Pretty.str c :: Pretty.str " ::" :: Pretty.brk 1 :: |
199 (Pretty.str c :: Pretty.str " ::" :: Pretty.brk 1 :: |
221 Pretty.commas (map prt_typ_no_tvars tys)); |
200 Pretty.commas (map prt_typ_no_tvars tys)); |
222 |
201 |
223 fun prt_axm (a, t) = Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, prt_term t]; |
202 fun prt_axm (a, t) = Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, prt_term t]; |
224 |
203 |
225 |
204 val {axioms, defs, oracles} = Theory.rep_theory thy; |
226 val {sign = _, defs, axioms, oracles, parents = _, ancestors = _} = Theory.rep_theory thy; |
205 val {naming, syn = _, tsig, consts} = Sign.rep_sg thy; |
227 val {self = _, tsig, consts, naming, data} = Sign.rep_sg sg; |
|
228 val {classes, default, types, arities, log_types = _, witness} = Type.rep_tsig tsig; |
206 val {classes, default, types, arities, log_types = _, witness} = Type.rep_tsig tsig; |
229 |
207 |
230 val clsses = NameSpace.extern_table (apsnd (Symtab.make o Graph.dest) classes); |
208 val clsses = NameSpace.extern_table (apsnd (Symtab.make o Graph.dest) classes); |
231 val tdecls = NameSpace.extern_table types; |
209 val tdecls = NameSpace.extern_table types; |
232 val cnsts = NameSpace.extern_table consts; |
210 val cnsts = NameSpace.extern_table consts; |
233 val finals = NameSpace.extern_table (#1 consts, Defs.finals defs); |
211 val finals = NameSpace.extern_table (#1 consts, Defs.finals defs); |
234 val axms = NameSpace.extern_table axioms; |
212 val axms = NameSpace.extern_table axioms; |
235 val oras = NameSpace.extern_table oracles; |
213 val oras = NameSpace.extern_table oracles; |
236 in |
214 in |
237 [Pretty.strs ("stamps:" :: Sign.stamp_names_of sg), |
215 [Pretty.strs ("names:" :: Context.names_of thy), |
238 Pretty.strs ("data:" :: Sign.data_kinds data), |
216 Pretty.strs ("data:" :: Context.theory_data thy), |
239 Pretty.strs ["name prefix:", NameSpace.path_of naming], |
217 Pretty.strs ["name prefix:", NameSpace.path_of naming], |
240 Pretty.big_list "classes:" (map pretty_classrel clsses), |
218 Pretty.big_list "classes:" (map pretty_classrel clsses), |
241 pretty_default default, |
219 pretty_default default, |
242 pretty_witness witness, |
220 pretty_witness witness, |
243 Pretty.big_list "syntactic types:" (List.mapPartial (pretty_type true) tdecls), |
221 Pretty.big_list "syntactic types:" (List.mapPartial (pretty_type true) tdecls), |