author  wenzelm 
Tue, 22 Oct 2019 20:59:57 +0200  
changeset 70924  15758fced053 
parent 64596  51f8e259de50 
child 74156  ecf80e37ed1a 
permissions  rwrr 
17369  1 
(* Title: Pure/Isar/proof_display.ML 
2 
Author: Makarius 

3 

19432
cae7cc072994
added print_theorems/theory, print_theorems_diff (from pure_thy.ML);
wenzelm
parents:
18799
diff
changeset

4 
Printing of theorems, goals, results etc. 
17369  5 
*) 
6 

7 
signature PROOF_DISPLAY = 

8 
sig 

30628  9 
val pp_context: Proof.context > Pretty.T 
60937  10 
val pp_thm: (unit > theory) > thm > Pretty.T 
11 
val pp_typ: (unit > theory) > typ > Pretty.T 

12 
val pp_term: (unit > theory) > term > Pretty.T 

13 
val pp_ctyp: (unit > theory) > ctyp > Pretty.T 

14 
val pp_cterm: (unit > theory) > cterm > Pretty.T 

61267  15 
val pretty_theory: bool > Proof.context > Pretty.T 
61252  16 
val pretty_definitions: bool > Proof.context > Pretty.T 
61266  17 
val pretty_theorems_diff: bool > theory list > Proof.context > Pretty.T list 
18 
val pretty_theorems: bool > Proof.context > Pretty.T list 

20311  19 
val string_of_rule: Proof.context > string > thm > string 
49860  20 
val pretty_goal_header: thm > Pretty.T 
21 
val string_of_goal: Proof.context > thm > string 

51584  22 
val pretty_goal_facts: Proof.context > string > thm list > Pretty.T 
49866  23 
val method_error: string > Position.T > 
24 
{context: Proof.context, facts: thm list, goal: thm} > 'a Seq.result 

56932
11a4001b06c6
more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56897
diff
changeset

25 
val print_results: bool > Position.T > Proof.context > 
11a4001b06c6
more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56897
diff
changeset

26 
((string * string) * (string * thm list) list) > unit 
11a4001b06c6
more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56897
diff
changeset

27 
val print_consts: bool > Position.T > Proof.context > 
11a4001b06c6
more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56897
diff
changeset

28 
(string * typ > bool) > (string * typ) list > unit 
17369  29 
end 
30 

33389  31 
structure Proof_Display: PROOF_DISPLAY = 
17369  32 
struct 
33 

61252  34 
(** toplevel pretty printing **) 
20211  35 

30628  36 
fun pp_context ctxt = 
42717
0bbb56867091
proper configuration options Proof_Context.debug and Proof_Context.verbose;
wenzelm
parents:
42360
diff
changeset

37 
(if Config.get ctxt Proof_Context.debug then 
42360  38 
Pretty.quote (Pretty.big_list "proof context:" (Proof_Context.pretty_context ctxt)) 
20211  39 
else Pretty.str "<context>"); 
40 

60937  41 
fun default_context mk_thy = 
62889  42 
(case Context.get_generic_context () of 
45269
6f8949e6c71a
more robust ML pretty printing (cf. b6c527c64789);
wenzelm
parents:
44240
diff
changeset

43 
SOME (Context.Proof ctxt) => ctxt 
6f8949e6c71a
more robust ML pretty printing (cf. b6c527c64789);
wenzelm
parents:
44240
diff
changeset

44 
 SOME (Context.Theory thy) => 
6f8949e6c71a
more robust ML pretty printing (cf. b6c527c64789);
wenzelm
parents:
44240
diff
changeset

45 
(case try Syntax.init_pretty_global thy of 
6f8949e6c71a
more robust ML pretty printing (cf. b6c527c64789);
wenzelm
parents:
44240
diff
changeset

46 
SOME ctxt => ctxt 
60937  47 
 NONE => Syntax.init_pretty_global (mk_thy ())) 
48 
 NONE => Syntax.init_pretty_global (mk_thy ())); 

49 

50 
fun pp_thm mk_thy th = 

61268  51 
Thm.pretty_thm_raw (default_context mk_thy) {quote = true, show_hyps = false} th; 
44240
4b1a63678839
improved default context for ML toplevel prettyprinting;
wenzelm
parents:
44192
diff
changeset

52 

60937  53 
fun pp_typ mk_thy T = Pretty.quote (Syntax.pretty_typ (default_context mk_thy) T); 
54 
fun pp_term mk_thy t = Pretty.quote (Syntax.pretty_term (default_context mk_thy) t); 

20211  55 

60937  56 
fun pp_ctyp mk_thy cT = pp_typ mk_thy (Thm.typ_of cT); 
57 
fun pp_cterm mk_thy ct = pp_term mk_thy (Thm.term_of ct); 

20211  58 

19432
cae7cc072994
added print_theorems/theory, print_theorems_diff (from pure_thy.ML);
wenzelm
parents:
18799
diff
changeset

59 

61252  60 

61 
(** theory content **) 

62 

61266  63 
fun pretty_theory verbose ctxt = 
64 
let 

65 
val thy = Proof_Context.theory_of ctxt; 

66 

67 
fun prt_cls c = Syntax.pretty_sort ctxt [c]; 

68 
fun prt_sort S = Syntax.pretty_sort ctxt S; 

69 
fun prt_arity t (c, Ss) = Syntax.pretty_arity ctxt (t, Ss, [c]); 

70 
fun prt_typ ty = Pretty.quote (Syntax.pretty_typ ctxt ty); 

71 
val prt_typ_no_tvars = prt_typ o Logic.unvarifyT_global; 

72 
fun prt_term t = Pretty.quote (Syntax.pretty_term ctxt t); 

73 
val prt_term_no_vars = prt_term o Logic.unvarify_global; 

74 
fun prt_const (c, ty) = [Pretty.mark_str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty]; 

75 

76 
fun pretty_classrel (c, []) = prt_cls c 

77 
 pretty_classrel (c, cs) = Pretty.block 

78 
(prt_cls c :: Pretty.str " <" :: Pretty.brk 1 :: Pretty.commas (map prt_cls cs)); 

79 

80 
fun pretty_default S = Pretty.block 

81 
[Pretty.str "default sort:", Pretty.brk 1, prt_sort S]; 

82 

83 
val tfrees = map (fn v => TFree (v, [])); 

84 
fun pretty_type syn (t, Type.LogicalType n) = 

85 
if syn then NONE 

86 
else SOME (prt_typ (Type (t, tfrees (Name.invent Name.context Name.aT n)))) 

87 
 pretty_type syn (t, Type.Abbreviation (vs, U, syn')) = 

88 
if syn <> syn' then NONE 

89 
else SOME (Pretty.block 

90 
[prt_typ (Type (t, tfrees vs)), Pretty.str " =", Pretty.brk 1, prt_typ U]) 

91 
 pretty_type syn (t, Type.Nonterminal) = 

92 
if not syn then NONE 

93 
else SOME (prt_typ (Type (t, []))); 

94 

95 
val pretty_arities = maps (fn (t, ars) => map (prt_arity t) ars); 

96 

97 
fun pretty_abbrev (c, (ty, t)) = Pretty.block 

64596  98 
(prt_const (c, ty) @ [Pretty.str " \<equiv>", Pretty.brk 1, prt_term_no_vars t]); 
19432
cae7cc072994
added print_theorems/theory, print_theorems_diff (from pure_thy.ML);
wenzelm
parents:
18799
diff
changeset

99 

61266  100 
fun pretty_axm (a, t) = 
101 
Pretty.block [Pretty.mark_str a, Pretty.str ":", Pretty.brk 1, prt_term_no_vars t]; 

102 

103 
val tsig = Sign.tsig_of thy; 

104 
val consts = Sign.consts_of thy; 

105 
val {const_space, constants, constraints} = Consts.dest consts; 

106 
val {classes, default, types, ...} = Type.rep_tsig tsig; 

107 
val type_space = Type.type_space tsig; 

108 
val (class_space, class_algebra) = classes; 

109 
val classes = Sorts.classes_of class_algebra; 

110 
val arities = Sorts.arities_of class_algebra; 

111 

112 
val clsses = 

113 
Name_Space.extern_entries verbose ctxt class_space 

114 
(map (fn ((c, _), cs) => (c, Sign.minimize_sort thy cs)) (Graph.dest classes)) 

115 
> map (apfst #1); 

116 
val tdecls = Name_Space.extern_table verbose ctxt types > map (apfst #1); 

117 
val arties = 

118 
Name_Space.extern_entries verbose ctxt type_space (Symtab.dest arities) 

119 
> map (apfst #1); 

120 

121 
val cnsts = Name_Space.markup_entries verbose ctxt const_space constants; 

122 
val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty)  _ => NONE) cnsts; 

123 
val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t))  _ => NONE) cnsts; 

124 
val cnstrs = Name_Space.markup_entries verbose ctxt const_space constraints; 

125 
in 

61267  126 
Pretty.chunks 
127 
[Pretty.big_list "classes:" (map pretty_classrel clsses), 

61266  128 
pretty_default default, 
129 
Pretty.big_list "syntactic types:" (map_filter (pretty_type true) tdecls), 

130 
Pretty.big_list "logical types:" (map_filter (pretty_type false) tdecls), 

131 
Pretty.big_list "type arities:" (pretty_arities arties), 

132 
Pretty.big_list "logical consts:" (map (Pretty.block o prt_const) log_cnsts), 

133 
Pretty.big_list "abbreviations:" (map pretty_abbrev abbrevs), 

134 
Pretty.big_list "constraints:" (map (Pretty.block o prt_const) cnstrs), 

135 
Pretty.block 

136 
(Pretty.breaks (Pretty.str "oracles:" :: 

61267  137 
map Pretty.mark_str (Thm.extern_oracles verbose ctxt)))] 
138 
end; 

139 

140 

141 
(* theorems *) 

142 

143 
fun pretty_theorems_diff verbose prev_thys ctxt = 

144 
let 

145 
val pretty_fact = Proof_Context.pretty_fact ctxt; 

146 
val facts = Global_Theory.facts_of (Proof_Context.theory_of ctxt); 

147 
val thmss = Facts.dest_static verbose (map Global_Theory.facts_of prev_thys) facts; 

148 
val prts = map #1 (sort_by (#1 o #2) (map (`pretty_fact) thmss)); 

149 
in if null prts then [] else [Pretty.big_list "theorems:" prts] end; 

150 

151 
fun pretty_theorems verbose ctxt = 

152 
pretty_theorems_diff verbose (Theory.parents_of (Proof_Context.theory_of ctxt)) ctxt; 

20621  153 

61252  154 

155 
(* definitions *) 

156 

157 
fun pretty_definitions verbose ctxt = 

158 
let 

159 
val thy = Proof_Context.theory_of ctxt; 

61261
ddb2da7cb2e4
more explicit Defs.context: use proper name spaces as far as possible;
wenzelm
parents:
61258
diff
changeset

160 
val context = Proof_Context.defs_context ctxt; 
61252  161 

61253  162 
val const_space = Proof_Context.const_space ctxt; 
163 
val type_space = Proof_Context.type_space ctxt; 

61256  164 
val item_space = fn Defs.Const => const_space  Defs.Type => type_space; 
61253  165 
fun prune_item (k, c) = not verbose andalso Name_Space.is_concealed (item_space k) c; 
166 

61261
ddb2da7cb2e4
more explicit Defs.context: use proper name spaces as far as possible;
wenzelm
parents:
61258
diff
changeset

167 
fun extern_item (kind, name) = 
ddb2da7cb2e4
more explicit Defs.context: use proper name spaces as far as possible;
wenzelm
parents:
61258
diff
changeset

168 
let val xname = Name_Space.extern ctxt (item_space kind) name 
ddb2da7cb2e4
more explicit Defs.context: use proper name spaces as far as possible;
wenzelm
parents:
61258
diff
changeset

169 
in (xname, (kind, name)) end; 
61253  170 

61261
ddb2da7cb2e4
more explicit Defs.context: use proper name spaces as far as possible;
wenzelm
parents:
61258
diff
changeset

171 
fun extern_item_ord ((xname1, (kind1, _)), (xname2, (kind2, _))) = 
ddb2da7cb2e4
more explicit Defs.context: use proper name spaces as far as possible;
wenzelm
parents:
61258
diff
changeset

172 
(case Defs.item_kind_ord (kind1, kind2) of 
ddb2da7cb2e4
more explicit Defs.context: use proper name spaces as far as possible;
wenzelm
parents:
61258
diff
changeset

173 
EQUAL => string_ord (xname1, xname2) 
ddb2da7cb2e4
more explicit Defs.context: use proper name spaces as far as possible;
wenzelm
parents:
61258
diff
changeset

174 
 ord => ord); 
61253  175 

61261
ddb2da7cb2e4
more explicit Defs.context: use proper name spaces as far as possible;
wenzelm
parents:
61258
diff
changeset

176 
fun sort_items f = sort (extern_item_ord o apply2 f); 
ddb2da7cb2e4
more explicit Defs.context: use proper name spaces as far as possible;
wenzelm
parents:
61258
diff
changeset

177 

ddb2da7cb2e4
more explicit Defs.context: use proper name spaces as far as possible;
wenzelm
parents:
61258
diff
changeset

178 
fun pretty_entry ((_: string, item), args) = Defs.pretty_entry context (item, args); 
61252  179 

180 
fun pretty_reduct (lhs, rhs) = Pretty.block 

61253  181 
([pretty_entry lhs, Pretty.str " >", Pretty.brk 2] @ 
182 
Pretty.commas (map pretty_entry (sort_items fst rhs))); 

61252  183 

61253  184 
fun pretty_restrict (entry, name) = 
185 
Pretty.block ([pretty_entry entry, Pretty.brk 2, Pretty.str ("(from " ^ quote name ^ ")")]); 

61252  186 

187 
val defs = Theory.defs_of thy; 

188 
val {restricts, reducts} = Defs.dest defs; 

22335  189 

61257  190 
val (reds1, reds2) = 
61253  191 
filter_out (prune_item o #1 o #1) reducts 
61252  192 
> map (fn (lhs, rhs) => 
61261
ddb2da7cb2e4
more explicit Defs.context: use proper name spaces as far as possible;
wenzelm
parents:
61258
diff
changeset

193 
(apfst extern_item lhs, map (apfst extern_item) (filter_out (prune_item o fst) rhs))) 
61253  194 
> sort_items (#1 o #1) 
61257  195 
> filter_out (null o #2) 
196 
> List.partition (Defs.plain_args o #2 o #1); 

61253  197 

61261
ddb2da7cb2e4
more explicit Defs.context: use proper name spaces as far as possible;
wenzelm
parents:
61258
diff
changeset

198 
val rests = restricts > map (apfst (apfst extern_item)) > sort_items (#1 o #1); 
61252  199 
in 
200 
Pretty.big_list "definitions:" 

61258  201 
(map (Pretty.text_fold o single) 
202 
[Pretty.big_list "nonoverloaded LHS:" (map pretty_reduct reds1), 

203 
Pretty.big_list "overloaded LHS:" (map pretty_reduct reds2), 

204 
Pretty.big_list "pattern restrictions due to incomplete LHS:" (map pretty_restrict rests)]) 

61252  205 
end; 
206 

207 

208 

209 
(** proof items **) 

19432
cae7cc072994
added print_theorems/theory, print_theorems_diff (from pure_thy.ML);
wenzelm
parents:
18799
diff
changeset

210 

17369  211 
(* refinement rule *) 
212 

213 
fun pretty_rule ctxt s thm = 

214 
Pretty.block [Pretty.str (s ^ " attempt to solve goal by exported rule:"), 

61268  215 
Pretty.fbrk, Thm.pretty_thm ctxt thm]; 
17369  216 

217 
val string_of_rule = Pretty.string_of ooo pretty_rule; 

218 

219 

49860  220 
(* goals *) 
221 

222 
local 

223 

224 
fun subgoals 0 = [] 

225 
 subgoals 1 = [Pretty.brk 1, Pretty.str "(1 subgoal)"] 

226 
 subgoals n = [Pretty.brk 1, Pretty.str ("(" ^ string_of_int n ^ " subgoals)")]; 

227 

228 
in 

229 

230 
fun pretty_goal_header goal = 

55763  231 
Pretty.block ([Pretty.keyword1 "goal"] @ subgoals (Thm.nprems_of goal) @ [Pretty.str ":"]); 
49860  232 

233 
end; 

234 

235 
fun string_of_goal ctxt goal = 

51958
bca32217b304
retain goal display options when printing error messages, to avoid breakdown for huge goals;
wenzelm
parents:
51601
diff
changeset

236 
Pretty.string_of (Pretty.chunks [pretty_goal_header goal, Goal_Display.pretty_goal ctxt goal]); 
49860  237 

238 

51584  239 
(* goal facts *) 
240 

241 
fun pretty_goal_facts ctxt s ths = 

242 
(Pretty.block o Pretty.fbreaks) 

51601  243 
[if s = "" then Pretty.str "this:" 
55763  244 
else Pretty.block [Pretty.keyword1 s, Pretty.brk 1, Pretty.str "this:"], 
51601  245 
Proof_Context.pretty_fact ctxt ("", ths)]; 
51584  246 

247 

49860  248 
(* method_error *) 
249 

49866  250 
fun method_error kind pos {context = ctxt, facts, goal} = Seq.Error (fn () => 
49860  251 
let 
49866  252 
val pr_header = 
253 
"Failed to apply " ^ (if kind = "" then "" else kind ^ " ") ^ 

254 
"proof method" ^ Position.here pos ^ ":\n"; 

49860  255 
val pr_facts = 
256 
if null facts then "" 

51584  257 
else Pretty.string_of (pretty_goal_facts ctxt "using" facts) ^ "\n"; 
49860  258 
val pr_goal = string_of_goal ctxt goal; 
259 
in pr_header ^ pr_facts ^ pr_goal end); 

260 

261 

17369  262 
(* results *) 
263 

56932
11a4001b06c6
more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56897
diff
changeset

264 
fun position_markup pos = Pretty.mark (Position.markup pos Markup.position); 
11a4001b06c6
more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56897
diff
changeset

265 

28092  266 
local 
267 

56932
11a4001b06c6
more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56897
diff
changeset

268 
fun pretty_fact_name pos (kind, "") = position_markup pos (Pretty.keyword1 kind) 
11a4001b06c6
more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56897
diff
changeset

269 
 pretty_fact_name pos (kind, name) = 
11a4001b06c6
more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56897
diff
changeset

270 
Pretty.block [position_markup pos (Pretty.keyword1 kind), Pretty.brk 1, 
41551  271 
Pretty.str (Long_Name.base_name name), Pretty.str ":"]; 
28087
a9cccdd9d521
pretty_fact/results: display base only, since results now come with full names (note that Facts.extern is not really welldefined unless we present the real target context);
wenzelm
parents:
27857
diff
changeset

272 

17369  273 
fun pretty_facts ctxt = 
55763  274 
flat o (separate [Pretty.fbrk, Pretty.keyword2 "and", Pretty.str " "]) o 
50126
3dec88149176
theorem status about oracles/futures is no longer printed by default;
wenzelm
parents:
49867
diff
changeset

275 
map (single o Proof_Context.pretty_fact ctxt); 
17369  276 

27857  277 
in 
278 

56932
11a4001b06c6
more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56897
diff
changeset

279 
fun print_results do_print pos ctxt ((kind, name), facts) = 
33643
b275f26a638b
eliminated obsolete "internal" kind  collapsed to unspecific "";
wenzelm
parents:
33515
diff
changeset

280 
if not do_print orelse kind = "" then () 
28092  281 
else if name = "" then 
59184
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
57605
diff
changeset

282 
(Output.state o Pretty.string_of) 
56932
11a4001b06c6
more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56897
diff
changeset

283 
(Pretty.block (position_markup pos (Pretty.keyword1 kind) :: Pretty.brk 1 :: 
11a4001b06c6
more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56897
diff
changeset

284 
pretty_facts ctxt facts)) 
46728
85f8e3932712
display proof results as "state", to suppress odd squiggles in the Prover IDE (see also 9240be8c8c69);
wenzelm
parents:
45269
diff
changeset

285 
else 
59184
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
57605
diff
changeset

286 
(Output.state o Pretty.string_of) 
46728
85f8e3932712
display proof results as "state", to suppress odd squiggles in the Prover IDE (see also 9240be8c8c69);
wenzelm
parents:
45269
diff
changeset

287 
(case facts of 
56932
11a4001b06c6
more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56897
diff
changeset

288 
[fact] => Pretty.blk (1, [pretty_fact_name pos (kind, name), Pretty.fbrk, 
50126
3dec88149176
theorem status about oracles/futures is no longer printed by default;
wenzelm
parents:
49867
diff
changeset

289 
Proof_Context.pretty_fact ctxt fact]) 
56932
11a4001b06c6
more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56897
diff
changeset

290 
 _ => Pretty.blk (1, [pretty_fact_name pos (kind, name), Pretty.fbrk, 
46728
85f8e3932712
display proof results as "state", to suppress odd squiggles in the Prover IDE (see also 9240be8c8c69);
wenzelm
parents:
45269
diff
changeset

291 
Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])])); 
17369  292 

293 
end; 

294 

20889  295 

296 
(* consts *) 

297 

298 
local 

299 

300 
fun pretty_var ctxt (x, T) = 

301 
Pretty.block [Pretty.str x, Pretty.str " ::", Pretty.brk 1, 

24920  302 
Pretty.quote (Syntax.pretty_typ ctxt T)]; 
20889  303 

56932
11a4001b06c6
more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56897
diff
changeset

304 
fun pretty_vars pos ctxt kind vs = 
62188  305 
Pretty.block 
306 
(Pretty.fbreaks (position_markup pos (Pretty.mark_str kind) :: map (pretty_var ctxt) vs)); 

307 

308 
val fixes = (Markup.keyword2, "fixes"); 

309 
val consts = (Markup.keyword1, "consts"); 

20889  310 

56932
11a4001b06c6
more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56897
diff
changeset

311 
fun pretty_consts pos ctxt pred cs = 
42360  312 
(case filter pred (#1 (Proof_Context.inferred_fixes ctxt)) of 
62188  313 
[] => pretty_vars pos ctxt consts cs 
314 
 ps => Pretty.chunks [pretty_vars pos ctxt fixes ps, pretty_vars pos ctxt consts cs]); 

20889  315 

44192
a32ca9165928
less verbosity in batch mode  spam reduction and notable performance improvement;
wenzelm
parents:
42717
diff
changeset

316 
in 
a32ca9165928
less verbosity in batch mode  spam reduction and notable performance improvement;
wenzelm
parents:
42717
diff
changeset

317 

56932
11a4001b06c6
more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56897
diff
changeset

318 
fun print_consts do_print pos ctxt pred cs = 
44192
a32ca9165928
less verbosity in batch mode  spam reduction and notable performance improvement;
wenzelm
parents:
42717
diff
changeset

319 
if not do_print orelse null cs then () 
59184
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
57605
diff
changeset

320 
else Output.state (Pretty.string_of (pretty_consts pos ctxt pred cs)); 
44192
a32ca9165928
less verbosity in batch mode  spam reduction and notable performance improvement;
wenzelm
parents:
42717
diff
changeset

321 

20889  322 
end; 
323 

17369  324 
end; 