# HG changeset patch
# User wenzelm
# Date 1288295941 -7200
# Node ID 39af96cc57cbf77f7a1e26cd0284158b087d44d4
# Parent  b9d15110b97ae55ea8ad7d2fdafad6c258d595d3
added Exn.interruptible_capture, which reraises interrupts as required by user-code (when Exn.capture is not immediately followed by Exn.release);
refined Exn.is_interrupt: detect nested IO Interrupts;
generalized Exn.map_result;
more precise dependencies;

diff -r b9d15110b97a -r 39af96cc57cb src/Pure/General/exn.ML
--- a/src/Pure/General/exn.ML	Thu Oct 28 21:52:33 2010 +0200
+++ b/src/Pure/General/exn.ML	Thu Oct 28 21:59:01 2010 +0200
@@ -11,12 +11,13 @@
   val get_exn: 'a result -> exn option
   val capture: ('a -> 'b) -> 'a -> 'b result
   val release: 'a result -> 'a
-  val map_result: ('a -> 'a) -> 'a result -> 'a result
+  val map_result: ('a -> 'b) -> 'a result -> 'b result
   exception Interrupt
   val interrupt: unit -> 'a
   val is_interrupt: exn -> bool
   val interrupt_exn: 'a result
   val is_interrupt_exn: 'a result -> bool
+  val interruptible_capture: ('a -> 'b) -> 'a -> 'b result
   exception EXCEPTIONS of exn list
   val flatten: exn -> exn list
   val flatten_list: exn list -> exn list
@@ -45,7 +46,7 @@
   | release (Exn e) = reraise e;
 
 fun map_result f (Result x) = Result (f x)
-  | map_result f e = e;
+  | map_result f (Exn e) = (Exn e);
 
 
 (* interrupts *)
@@ -55,7 +56,7 @@
 fun interrupt () = raise Interrupt;
 
 fun is_interrupt Interrupt = true
-  | is_interrupt (IO.Io {cause = Interrupt, ...}) = true
+  | is_interrupt (IO.Io {cause, ...}) = is_interrupt cause
   | is_interrupt _ = false;
 
 val interrupt_exn = Exn Interrupt;
@@ -63,6 +64,9 @@
 fun is_interrupt_exn (Exn exn) = is_interrupt exn
   | is_interrupt_exn _ = false;
 
+fun interruptible_capture f x =
+  Result (f x) handle e => if is_interrupt e then reraise e else Exn e;
+
 
 (* nested exceptions *)
 
diff -r b9d15110b97a -r 39af96cc57cb src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Thu Oct 28 21:52:33 2010 +0200
+++ b/src/Pure/IsaMakefile	Thu Oct 28 21:59:01 2010 +0200
@@ -20,6 +20,7 @@
 ## Pure
 
 BOOTSTRAP_FILES = 					\
+  General/exn.ML					\
   ML-Systems/bash.ML 					\
   ML-Systems/compiler_polyml-5.2.ML			\
   ML-Systems/compiler_polyml-5.3.ML			\
@@ -73,7 +74,6 @@
   General/basics.ML					\
   General/binding.ML					\
   General/buffer.ML					\
-  General/exn.ML					\
   General/file.ML					\
   General/graph.ML					\
   General/heap.ML					\