303 fun pretty_var ctxt (x, T) = |
303 fun pretty_var ctxt (x, T) = |
304 Pretty.block [Pretty.str x, Pretty.str " ::", Pretty.brk 1, |
304 Pretty.block [Pretty.str x, Pretty.str " ::", Pretty.brk 1, |
305 Pretty.quote (Syntax.pretty_typ ctxt T)]; |
305 Pretty.quote (Syntax.pretty_typ ctxt T)]; |
306 |
306 |
307 fun pretty_vars pos ctxt kind vs = |
307 fun pretty_vars pos ctxt kind vs = |
308 Pretty.block (Pretty.fbreaks (position_markup pos (Pretty.str kind) :: map (pretty_var ctxt) vs)); |
308 Pretty.block |
|
309 (Pretty.fbreaks (position_markup pos (Pretty.mark_str kind) :: map (pretty_var ctxt) vs)); |
|
310 |
|
311 val fixes = (Markup.keyword2, "fixes"); |
|
312 val consts = (Markup.keyword1, "consts"); |
309 |
313 |
310 fun pretty_consts pos ctxt pred cs = |
314 fun pretty_consts pos ctxt pred cs = |
311 (case filter pred (#1 (Proof_Context.inferred_fixes ctxt)) of |
315 (case filter pred (#1 (Proof_Context.inferred_fixes ctxt)) of |
312 [] => pretty_vars pos ctxt "constants" cs |
316 [] => pretty_vars pos ctxt consts cs |
313 | ps => Pretty.chunks [pretty_vars pos ctxt "parameters" ps, pretty_vars pos ctxt "constants" cs]); |
317 | ps => Pretty.chunks [pretty_vars pos ctxt fixes ps, pretty_vars pos ctxt consts cs]); |
314 |
318 |
315 in |
319 in |
316 |
320 |
317 fun print_consts do_print pos ctxt pred cs = |
321 fun print_consts do_print pos ctxt pred cs = |
318 if not do_print orelse null cs then () |
322 if not do_print orelse null cs then () |