src/Pure/RAW/exn.ML

 end;
 
 signature EXN =
 sig
   include BASIC_EXN
+  val reraise: exn -> 'a
   datatype 'a result = Res of 'a | Exn of exn
   val get_res: 'a result -> 'a option
   val get_exn: 'a result -> exn option
   val capture: ('a -> 'b) -> 'a -> 'b result
   val release: 'a result -> 'a

   val is_interrupt_exn: 'a result -> bool
   val interruptible_capture: ('a -> 'b) -> 'a -> 'b result
   val return_code: exn -> int -> int
   val capture_exit: int -> ('a -> 'b) -> 'a -> 'b
   exception EXCEPTIONS of exn list
+  val trace: (exn -> string) -> (string -> unit) -> (unit -> 'a) -> 'a
 end;
 
 structure Exn: EXN =
 struct
+
+(* reraise *)
+
+fun reraise exn =
+  (case PolyML.exceptionLocation exn of
+    NONE => raise exn
+  | SOME location => PolyML.raiseWithLocation (exn, location));
+
 
 (* user errors *)
 
 exception ERROR of string;
 

   | map_exn f (Exn e) = Exn (f e);
 
 
 (* interrupts *)
 
-exception Interrupt = Interrupt;
+exception Interrupt = SML90.Interrupt;
 
 fun interrupt () = raise Interrupt;
 
 fun is_interrupt Interrupt = true
   | is_interrupt (IO.Io {cause, ...}) = is_interrupt cause

 
 (* concatenated exceptions *)
 
 exception EXCEPTIONS of exn list;
 
+
+(* low-level trace *)
+
+fun trace exn_message output e =
+  PolyML.Exception.traceException
+    (e, fn (trace, exn) =>
+      let
+        val title = "Exception trace - " ^ exn_message exn;
+        val () = output (String.concatWith "\n" (title :: trace));
+      in reraise exn end);
+
 end;
 
 datatype illegal = Interrupt;
 
 structure Basic_Exn: BASIC_EXN = Exn;