--- a/src/Pure/General/basics.ML Sat Jun 06 21:46:36 2009 +0200
+++ b/src/Pure/General/basics.ML Sat Jun 06 21:47:02 2009 +0200
@@ -94,7 +94,7 @@
(* partiality *)
fun try f x = SOME (f x)
- handle Exn.Interrupt => raise Exn.Interrupt | _ => NONE;
+ handle (exn as Exn.Interrupt) => reraise exn | _ => NONE;
fun can f x = is_some (try f x);
--- a/src/Pure/ML-Systems/compiler_polyml-5.0.ML Sat Jun 06 21:46:36 2009 +0200
+++ b/src/Pure/ML-Systems/compiler_polyml-5.0.ML Sat Jun 06 21:47:02 2009 +0200
@@ -21,7 +21,7 @@
[] => ()
| _ => (PolyML.compilerEx (get, put, fn () => ! current_line, name) (); exec ()));
in
- exec () handle exn => (error (output ()); raise exn);
+ exec () handle exn => (error (output ()); reraise exn);
if verbose then print (output ()) else ()
end;
--- a/src/Pure/ML-Systems/compiler_polyml-5.2.ML Sat Jun 06 21:46:36 2009 +0200
+++ b/src/Pure/ML-Systems/compiler_polyml-5.2.ML Sat Jun 06 21:47:02 2009 +0200
@@ -38,7 +38,7 @@
PolyML.compiler (get, parameters) ())
handle exn =>
(put ("Exception- " ^ General.exnMessage exn ^ " raised");
- error (output ()); raise exn);
+ error (output ()); reraise exn);
in if verbose then print (output ()) else () end;
fun use_file context verbose name =
--- a/src/Pure/ML-Systems/compiler_polyml-5.3.ML Sat Jun 06 21:46:36 2009 +0200
+++ b/src/Pure/ML-Systems/compiler_polyml-5.3.ML Sat Jun 06 21:47:02 2009 +0200
@@ -42,7 +42,7 @@
PolyML.compiler (get, parameters) ())
handle exn =>
(put ("Exception- " ^ General.exnMessage exn ^ " raised");
- error (output ()); raise exn);
+ error (output ()); reraise exn);
in if verbose then print (output ()) else () end;
fun use_file context verbose name =
--- a/src/Pure/ML/ml_compiler_polyml-5.3.ML Sat Jun 06 21:46:36 2009 +0200
+++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML Sat Jun 06 21:47:02 2009 +0200
@@ -173,7 +173,7 @@
PolyML.compiler (get, parameters) ())
handle exn =>
(put ("Exception- " ^ General.exnMessage exn ^ " raised");
- err (output ()); raise exn);
+ err (output ()); reraise exn);
in if verbose then print (output ()) else () end;
end;