equal
deleted
inserted
replaced
31 val prompt_state_fn: (state -> string) ref |
31 val prompt_state_fn: (state -> string) ref |
32 val print_state_context: state -> unit |
32 val print_state_context: state -> unit |
33 val print_state_default: bool -> state -> unit |
33 val print_state_default: bool -> state -> unit |
34 val print_state_fn: (bool -> state -> unit) ref |
34 val print_state_fn: (bool -> state -> unit) ref |
35 val print_state: bool -> state -> unit |
35 val print_state: bool -> state -> unit |
36 val print_exn_fn: ((exn * string) option -> unit) ref |
|
37 val print_exn_str: (exn * string) option -> string option |
|
38 val pretty_state: bool -> state -> Pretty.T list |
36 val pretty_state: bool -> state -> Pretty.T list |
39 val quiet: bool ref |
37 val quiet: bool ref |
40 val debug: bool ref |
38 val debug: bool ref |
41 val interact: bool ref |
39 val interact: bool ref |
42 val timing: bool ref |
40 val timing: bool ref |
310 and fail_msg detailed kind ((name, pos), exn) = |
308 and fail_msg detailed kind ((name, pos), exn) = |
311 "Error in " ^ kind ^ " " ^ quote name ^ Position.str_of pos ^ ":\n" ^ exn_msg detailed exn; |
309 "Error in " ^ kind ^ " " ^ quote name ^ Position.str_of pos ^ ":\n" ^ exn_msg detailed exn; |
312 |
310 |
313 in |
311 in |
314 |
312 |
315 |
|
316 |
|
317 fun exn_message exn = exn_msg (! debug) exn; |
313 fun exn_message exn = exn_msg (! debug) exn; |
318 |
314 |
319 fun print_exn_str NONE = NONE |
315 fun print_exn NONE = () |
320 | print_exn_str (SOME (exn, s)) = SOME (cat_lines [exn_message exn, s]); |
316 | print_exn (SOME (exn, s)) = Output.error_msg (cat_lines [exn_message exn, s]); |
321 |
|
322 val print_exn_default = K () o Option.map Output.error_msg o print_exn_str |
|
323 |
|
324 val print_exn_fn = ref print_exn_default; |
|
325 |
317 |
326 end; |
318 end; |
327 |
319 |
328 |
320 |
329 (* controlled execution *) |
321 (* controlled execution *) |
745 fun >> tr = |
737 fun >> tr = |
746 (case apply true tr (get_state ()) of |
738 (case apply true tr (get_state ()) of |
747 NONE => false |
739 NONE => false |
748 | SOME (state', exn_info) => |
740 | SOME (state', exn_info) => |
749 (global_state := (state', exn_info); |
741 (global_state := (state', exn_info); |
750 !print_exn_fn exn_info; |
742 print_exn exn_info; |
751 true)); |
743 true)); |
752 |
744 |
753 fun >>> [] = () |
745 fun >>> [] = () |
754 | >>> (tr :: trs) = if >> tr then >>> trs else (); |
746 | >>> (tr :: trs) = if >> tr then >>> trs else (); |
755 |
747 |