follow updates of Isabelle/Pure;
authorwenzelm
Thu, 18 Aug 2011 00:02:44 +0200
changeset 45129a93426812ad5
parent 45128 5f202ae4340c
child 45133 355d5438f5fb
follow updates of Isabelle/Pure;
Admin/polyml/future/ROOT.ML
     1.1 --- a/Admin/polyml/future/ROOT.ML	Wed Aug 17 23:41:47 2011 +0200
     1.2 +++ b/Admin/polyml/future/ROOT.ML	Thu Aug 18 00:02:44 2011 +0200
     1.3 @@ -7,6 +7,22 @@
     1.4      NONE => raise exn
     1.5    | SOME location => PolyML.raiseWithLocation (exn, location));
     1.6  
     1.7 +fun set_exn_serial i exn =
     1.8 +  let
     1.9 +    val (file, startLine, endLine) =
    1.10 +      (case PolyML.exceptionLocation exn of
    1.11 +        NONE => ("", 0, 0)
    1.12 +      | SOME {file, startLine, endLine, startPosition, ...} => (file, startLine, endLine));
    1.13 +    val location =
    1.14 +      {file = file, startLine = startLine, endLine = endLine,
    1.15 +        startPosition = ~ i, endPosition = 0};
    1.16 +  in PolyML.raiseWithLocation (exn, location) handle e => e end;
    1.17 +
    1.18 +fun get_exn_serial exn =
    1.19 +  (case Option.map #startPosition (PolyML.exceptionLocation exn) of
    1.20 +    NONE => NONE
    1.21 +  | SOME i => if i >= 0 then NONE else SOME (~ i));
    1.22 +
    1.23  exception Interrupt = SML90.Interrupt;
    1.24  val ord = SML90.ord;
    1.25  val chr = SML90.chr;
    1.26 @@ -61,6 +77,7 @@
    1.27  use "General/alist.ML";
    1.28  use "General/table.ML";
    1.29  use "General/graph.ML";
    1.30 +use "General/ord_list.ML";
    1.31  
    1.32  structure Position =
    1.33  struct
    1.34 @@ -89,6 +106,7 @@
    1.35  use "General/markup.ML";
    1.36  use "Concurrent/single_assignment.ML";
    1.37  use "Concurrent/time_limit.ML";
    1.38 +use "Concurrent/par_exn.ML";
    1.39  use "Concurrent/task_queue.ML";
    1.40  use "Concurrent/future.ML";
    1.41  use "Concurrent/lazy.ML";