follow updates of Isabelle/Pure;
authorwenzelm
Thu, 18 Aug 2011 00:02:44 +0200
changeset 44258 a93426812ad5
parent 44257 5f202ae4340c
child 44262 355d5438f5fb
follow updates of Isabelle/Pure;
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";