# HG changeset patch
# User wenzelm
# Date 1244317622 -7200
# Node ID 05937d6aafb5ee8409590e4e2c53c60d9224df99
# Parent  08e2a70d002a1f36dd2299e60a78433796728c59
reraise exceptions to preserve position information;

diff -r 08e2a70d002a -r 05937d6aafb5 src/Pure/General/basics.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);
 
diff -r 08e2a70d002a -r 05937d6aafb5 src/Pure/ML-Systems/compiler_polyml-5.0.ML
--- 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;
 
diff -r 08e2a70d002a -r 05937d6aafb5 src/Pure/ML-Systems/compiler_polyml-5.2.ML
--- 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 =
diff -r 08e2a70d002a -r 05937d6aafb5 src/Pure/ML-Systems/compiler_polyml-5.3.ML
--- 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 =
diff -r 08e2a70d002a -r 05937d6aafb5 src/Pure/ML/ml_compiler_polyml-5.3.ML
--- 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;