equal
deleted
inserted
replaced
16 val print_theorems: bool -> theory -> unit |
16 val print_theorems: bool -> theory -> unit |
17 val pretty_full_theory: bool -> theory -> Pretty.T |
17 val pretty_full_theory: bool -> theory -> Pretty.T |
18 val print_theory: theory -> unit |
18 val print_theory: theory -> unit |
19 val string_of_rule: Proof.context -> string -> thm -> string |
19 val string_of_rule: Proof.context -> string -> thm -> string |
20 val print_results: bool -> Proof.context -> ((string * string) * (string * thm list) list) -> unit |
20 val print_results: bool -> Proof.context -> ((string * string) * (string * thm list) list) -> unit |
21 val pretty_consts: Proof.context -> (string * typ -> bool) -> (string * typ) list -> Pretty.T |
21 val print_consts: bool -> Proof.context -> (string * typ -> bool) -> (string * typ) list -> unit |
22 end |
22 end |
23 |
23 |
24 structure Proof_Display: PROOF_DISPLAY = |
24 structure Proof_Display: PROOF_DISPLAY = |
25 struct |
25 struct |
26 |
26 |
113 Pretty.block [Pretty.str x, Pretty.str " ::", Pretty.brk 1, |
113 Pretty.block [Pretty.str x, Pretty.str " ::", Pretty.brk 1, |
114 Pretty.quote (Syntax.pretty_typ ctxt T)]; |
114 Pretty.quote (Syntax.pretty_typ ctxt T)]; |
115 |
115 |
116 fun pretty_vars ctxt kind vs = Pretty.big_list kind (map (pretty_var ctxt) vs); |
116 fun pretty_vars ctxt kind vs = Pretty.big_list kind (map (pretty_var ctxt) vs); |
117 |
117 |
118 in |
|
119 |
|
120 fun pretty_consts ctxt pred cs = |
118 fun pretty_consts ctxt pred cs = |
121 (case filter pred (#1 (Proof_Context.inferred_fixes ctxt)) of |
119 (case filter pred (#1 (Proof_Context.inferred_fixes ctxt)) of |
122 [] => pretty_vars ctxt "constants" cs |
120 [] => pretty_vars ctxt "constants" cs |
123 | ps => Pretty.chunks [pretty_vars ctxt "parameters" ps, pretty_vars ctxt "constants" cs]); |
121 | ps => Pretty.chunks [pretty_vars ctxt "parameters" ps, pretty_vars ctxt "constants" cs]); |
124 |
122 |
|
123 in |
|
124 |
|
125 fun print_consts do_print ctxt pred cs = |
|
126 if not do_print orelse null cs then () |
|
127 else Pretty.writeln (pretty_consts ctxt pred cs); |
|
128 |
125 end; |
129 end; |
126 |
130 |
127 end; |
131 end; |