# HG changeset patch
# User wenzelm
# Date 1244129498 -7200
# Node ID 5a07cc86675d1d7d615ba6473e6fd2f25e282203
# Parent  5c9dbd5115109ff1fd15b8c64c4758e251bb9307
reraise exceptions to preserve original position (ML system specific);

diff -r 5c9dbd511510 -r 5a07cc86675d src/Pure/ML-Systems/exn.ML
--- a/src/Pure/ML-Systems/exn.ML	Thu Jun 04 17:31:37 2009 +0200
+++ b/src/Pure/ML-Systems/exn.ML	Thu Jun 04 17:31:38 2009 +0200
@@ -35,7 +35,7 @@
 fun capture f x = Result (f x) handle e => Exn e;
 
 fun release (Result y) = y
-  | release (Exn e) = raise e;
+  | release (Exn e) = reraise e;
 
 
 (* interrupt and nested exceptions *)
@@ -58,6 +58,6 @@
     | exns => raise EXCEPTIONS exns);
 
 fun release_first results = release_all results
-  handle EXCEPTIONS (exn :: _) => raise exn;
+  handle EXCEPTIONS (exn :: _) => reraise exn;
 
 end;
diff -r 5c9dbd511510 -r 5a07cc86675d src/Pure/ML-Systems/mosml.ML
--- a/src/Pure/ML-Systems/mosml.ML	Thu Jun 04 17:31:37 2009 +0200
+++ b/src/Pure/ML-Systems/mosml.ML	Thu Jun 04 17:31:38 2009 +0200
@@ -38,6 +38,7 @@
 load "CharVector";
 
 exception Interrupt;
+fun reraise exn = raise exn;
 
 use "ML-Systems/exn.ML";
 use "ML-Systems/universal.ML";
diff -r 5c9dbd511510 -r 5a07cc86675d src/Pure/ML-Systems/polyml-5.0.ML
--- a/src/Pure/ML-Systems/polyml-5.0.ML	Thu Jun 04 17:31:37 2009 +0200
+++ b/src/Pure/ML-Systems/polyml-5.0.ML	Thu Jun 04 17:31:38 2009 +0200
@@ -3,6 +3,8 @@
 Compatibility wrapper for Poly/ML 5.0.
 *)
 
+fun reraise exn = raise exn;
+
 use "ML-Systems/universal.ML";
 use "ML-Systems/thread_dummy.ML";
 use "ML-Systems/ml_name_space.ML";
diff -r 5c9dbd511510 -r 5a07cc86675d src/Pure/ML-Systems/polyml-5.1.ML
--- a/src/Pure/ML-Systems/polyml-5.1.ML	Thu Jun 04 17:31:37 2009 +0200
+++ b/src/Pure/ML-Systems/polyml-5.1.ML	Thu Jun 04 17:31:38 2009 +0200
@@ -3,6 +3,8 @@
 Compatibility wrapper for Poly/ML 5.1.
 *)
 
+fun reraise exn = raise exn;
+
 use "ML-Systems/thread_dummy.ML";
 use "ML-Systems/ml_name_space.ML";
 use "ML-Systems/polyml_common.ML";
diff -r 5c9dbd511510 -r 5a07cc86675d src/Pure/ML-Systems/polyml-experimental.ML
--- a/src/Pure/ML-Systems/polyml-experimental.ML	Thu Jun 04 17:31:37 2009 +0200
+++ b/src/Pure/ML-Systems/polyml-experimental.ML	Thu Jun 04 17:31:38 2009 +0200
@@ -12,6 +12,11 @@
   val global = PolyML.globalNameSpace;
 end;
 
+fun reraise exn =
+  (case PolyML.exceptionLocation exn of
+    NONE => raise exn
+  | SOME location => PolyML.raiseWithLocation (exn, location));
+
 use "ML-Systems/polyml_common.ML";
 use "ML-Systems/multithreading_polyml.ML";
 
diff -r 5c9dbd511510 -r 5a07cc86675d src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Thu Jun 04 17:31:37 2009 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Thu Jun 04 17:31:38 2009 +0200
@@ -12,6 +12,8 @@
   val global = PolyML.globalNameSpace;
 end;
 
+fun reraise exn = raise exn;
+
 use "ML-Systems/polyml_common.ML";
 
 if ml_system = "polyml-5.2"
diff -r 5c9dbd511510 -r 5a07cc86675d src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/smlnj.ML	Thu Jun 04 17:31:37 2009 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Thu Jun 04 17:31:38 2009 +0200
@@ -4,6 +4,7 @@
 *)
 
 exception Interrupt;
+fun reraise exn = raise exn;
 
 use "ML-Systems/proper_int.ML";
 use "ML-Systems/overloading_smlnj.ML";