src/Pure/ML/ml_compiler.ML

 *)
 
 signature ML_COMPILER =
 sig
   type flags =
-    {environment: string, redirect: bool, verbose: bool,
+    {environment: string, redirect: bool, verbose: bool, catch_all: bool,
       debug: bool option, writeln: string -> unit, warning: string -> unit}
   val debug_flags: bool option -> flags
   val flags: flags
   val verbose: bool -> flags -> flags
+  val ML_catch_all: bool Config.T
   val eval: flags -> Position.T -> ML_Lex.token list -> unit
 end;
 
 structure ML_Compiler: ML_COMPILER =
 struct
 
 (* flags *)
 
 type flags =
-  {environment: string, redirect: bool, verbose: bool,
+  {environment: string, redirect: bool, verbose: bool, catch_all: bool,
     debug: bool option, writeln: string -> unit, warning: string -> unit};
 
 fun debug_flags opt_debug : flags =
-  {environment = "", redirect = false, verbose = false,
+  {environment = "", redirect = false, verbose = false, catch_all = false,
     debug = opt_debug, writeln = writeln, warning = warning};
 
 val flags = debug_flags NONE;
 
-fun verbose b (flags: flags) =
-  {environment = #environment flags, redirect = #redirect flags, verbose = b,
-    debug = #debug flags, writeln = #writeln flags, warning = #warning flags};
+fun verbose b ({environment, redirect, verbose = _, catch_all, debug, writeln, warning}: flags) =
+  {environment = environment, redirect = redirect, verbose = b, catch_all = catch_all,
+    debug = debug, writeln = writeln, warning = warning};
 
 
 (* parse trees *)
 
 fun breakpoint_position loc =

  in map (fn (_, (id, (b, pos))) => (id, (b, Position.dest pos))) all_breakpoints end;
 
 
 (* eval ML source tokens *)
 
+val ML_catch_all = Config.declare_bool ("ML_catch_all", \<^here>) (K false);
+
 fun eval (flags: flags) pos toks =
   let
     val opt_context = Context.get_generic_context ();
 
     val env as {debug, name_space, add_breakpoints} =

       in if is_err then error (trim_line msg) else () end;
 
     fun message {message = msg, hard, location = loc, context = _} =
       let
         val pos = Exn_Properties.position_of_polyml_location loc;
-        val txt =
-          (if hard then "ML error" else "ML warning") ^ Position.here pos ^ ":\n" ^
-          Pretty.string_of (Pretty.from_polyml msg);
-      in if hard then err txt else warn txt end;
+        val s = Pretty.string_of (Pretty.from_polyml msg);
+        val catch_all =
+          #catch_all flags orelse
+            (case opt_context of
+              NONE => false
+            | SOME context => Config.get_generic context ML_catch_all);
+        val is_err =
+          hard orelse
+            (not catch_all andalso
+              String.isPrefix "Handler catches all exceptions" (XML.content_of (YXML.parse_body s)));
+        val txt = (if is_err then "ML error" else "ML warning") ^ Position.here pos ^ ":\n" ^ s;
+      in if is_err then err txt else warn txt end;
 
 
     (* results *)
 
     val depth = FixedInt.fromInt (ML_Print_Depth.get_print_depth ());