Expose command failure recovery code for top level.
authoraspinall
Wed Jan 03 21:09:13 2007 +0100 (2007-01-03)
changeset 21982fe30893e50f2
parent 21981 4bb32c127529
child 21983 9fb029d1189b
Expose command failure recovery code for top level.
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Wed Jan 03 21:00:24 2007 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Jan 03 21:09:13 2007 +0100
     1.3 @@ -33,6 +33,8 @@
     1.4    val print_state_default: bool -> state -> unit
     1.5    val print_state_fn: (bool -> state -> unit) ref
     1.6    val print_state: bool -> state -> unit
     1.7 +  val print_exn_fn: ((exn * string) option -> unit) ref
     1.8 +  val print_exn_str: (exn * string) option -> string option
     1.9    val pretty_state: bool -> state -> Pretty.T list
    1.10    val quiet: bool ref
    1.11    val debug: bool ref
    1.12 @@ -310,10 +312,16 @@
    1.13  
    1.14  in
    1.15  
    1.16 +
    1.17 +
    1.18  fun exn_message exn = exn_msg (! debug) exn;
    1.19  
    1.20 -fun print_exn NONE = ()
    1.21 -  | print_exn (SOME (exn, s)) = Output.error_msg (cat_lines [exn_message exn, s]);
    1.22 +fun print_exn_str NONE = NONE
    1.23 +  | print_exn_str (SOME (exn, s)) = SOME (cat_lines [exn_message exn, s]);
    1.24 +
    1.25 +val print_exn_default = Option.app Output.error_msg o print_exn_str
    1.26 +
    1.27 +val print_exn_fn = ref print_exn_default;
    1.28  
    1.29  end;
    1.30  
    1.31 @@ -739,7 +747,7 @@
    1.32      NONE => false
    1.33    | SOME (state', exn_info) =>
    1.34        (global_state := (state', exn_info);
    1.35 -        print_exn exn_info;
    1.36 +        !print_exn_fn exn_info;
    1.37          true));
    1.38  
    1.39  fun >>> [] = ()