# HG changeset patch
# User wenzelm
# Date 1313618564 -7200
# Node ID a93426812ad5ef0765e0dcb980937e759ffb99f4
# Parent  5f202ae4340cf43cc6cef74ad6e03d32fd5c34a0
follow updates of Isabelle/Pure;

diff -r 5f202ae4340c -r a93426812ad5 Admin/polyml/future/ROOT.ML
--- a/Admin/polyml/future/ROOT.ML	Wed Aug 17 23:41:47 2011 +0200
+++ b/Admin/polyml/future/ROOT.ML	Thu Aug 18 00:02:44 2011 +0200
@@ -7,6 +7,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));
+
 exception Interrupt = SML90.Interrupt;
 val ord = SML90.ord;
 val chr = SML90.chr;
@@ -61,6 +77,7 @@
 use "General/alist.ML";
 use "General/table.ML";
 use "General/graph.ML";
+use "General/ord_list.ML";
 
 structure Position =
 struct
@@ -89,6 +106,7 @@
 use "General/markup.ML";
 use "Concurrent/single_assignment.ML";
 use "Concurrent/time_limit.ML";
+use "Concurrent/par_exn.ML";
 use "Concurrent/task_queue.ML";
 use "Concurrent/future.ML";
 use "Concurrent/lazy.ML";