equal
deleted
inserted
replaced
31 val enter_proof_body: state -> Proof.state |
31 val enter_proof_body: state -> Proof.state |
32 val prompt_state_default: state -> string |
32 val prompt_state_default: state -> string |
33 val prompt_state_fn: (state -> string) ref |
33 val prompt_state_fn: (state -> string) ref |
34 val print_state_context: state -> unit |
34 val print_state_context: state -> unit |
35 val print_state_default: bool -> state -> unit |
35 val print_state_default: bool -> state -> unit |
36 val print_state_hook: (bool -> state -> unit) -> unit |
|
37 val print_state_fn: (bool -> state -> unit) ref |
36 val print_state_fn: (bool -> state -> unit) ref |
38 val print_state: bool -> state -> unit |
37 val print_state: bool -> state -> unit |
39 val pretty_state: bool -> state -> Pretty.T list |
38 val pretty_state: bool -> state -> Pretty.T list |
40 val quiet: bool ref |
39 val quiet: bool ref |
41 val debug: bool ref |
40 val debug: bool ref |
220 end; |
219 end; |
221 |
220 |
222 val print_state_context = Pretty.writelns o pretty_state_context; |
221 val print_state_context = Pretty.writelns o pretty_state_context; |
223 fun print_state_default prf_only state = Pretty.writelns (pretty_state prf_only state); |
222 fun print_state_default prf_only state = Pretty.writelns (pretty_state prf_only state); |
224 |
223 |
225 val print_state_hooks = ref ([]: (bool -> state -> unit) list); |
|
226 fun print_state_hook f = change print_state_hooks (cons f); |
|
227 val print_state_fn = ref print_state_default; |
224 val print_state_fn = ref print_state_default; |
228 |
225 fun print_state prf_only state = ! print_state_fn prf_only state; |
229 fun print_state prf_only state = |
|
230 (List.app (fn f => (try (fn () => f prf_only state) (); ())) (! print_state_hooks); |
|
231 ! print_state_fn prf_only state); |
|
232 |
226 |
233 |
227 |
234 |
228 |
235 (** toplevel transitions **) |
229 (** toplevel transitions **) |
236 |
230 |