reraise exceptions to preserve position information;
authorwenzelm
Sat, 06 Jun 2009 21:47:02 +0200
changeset 31480 05937d6aafb5
parent 31479 08e2a70d002a
child 31495 a153d2de112c
reraise exceptions to preserve position information;
src/Pure/General/basics.ML
src/Pure/ML-Systems/compiler_polyml-5.0.ML
src/Pure/ML-Systems/compiler_polyml-5.2.ML
src/Pure/ML-Systems/compiler_polyml-5.3.ML
src/Pure/ML/ml_compiler_polyml-5.3.ML
--- 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;