src/Pure/ML-Systems/polyml.ML

--- a/src/Pure/ML-Systems/polyml.ML	Wed Aug 17 15:03:30 2011 -0700
+++ b/src/Pure/ML-Systems/polyml.ML	Wed Aug 17 15:12:34 2011 -0700
@@ -17,6 +17,22 @@
     NONE => raise exn
   | SOME location => PolyML.raiseWithLocation (exn, location));
 
+fun set_exn_serial i exn =
+  let
+    val (file, startLine, endLine) =
+      (case PolyML.exceptionLocation exn of
+        NONE => ("", 0, 0)
+      | SOME {file, startLine, endLine, startPosition, ...} => (file, startLine, endLine));
+    val location =
+      {file = file, startLine = startLine, endLine = endLine,
+        startPosition = ~ i, endPosition = 0};
+  in PolyML.raiseWithLocation (exn, location) handle e => e end;
+
+fun get_exn_serial exn =
+  (case Option.map #startPosition (PolyML.exceptionLocation exn) of
+    NONE => NONE
+  | SOME i => if i >= 0 then NONE else SOME (~ i));
+
 use "ML-Systems/polyml_common.ML";
 use "ML-Systems/multithreading_polyml.ML";
 use "ML-Systems/unsynchronized.ML";