# HG changeset patch
# User wenzelm
# Date 1222855202 -7200
# Node ID de653f1ad78b4b322d03dca00a59ab6fba33a2c1
# Parent  bd9573735bdd66f396d6e0c91e118331054d294e
more robust treatment of Interrupt (cf. exn.ML);

diff -r bd9573735bdd -r de653f1ad78b src/Pure/Concurrent/mailbox.ML
--- a/src/Pure/Concurrent/mailbox.ML	Wed Oct 01 12:00:01 2008 +0200
+++ b/src/Pure/Concurrent/mailbox.ML	Wed Oct 01 12:00:02 2008 +0200
@@ -52,7 +52,7 @@
       fun check () = not (Queue.is_empty (! messages)) orelse
         ConditionVar.waitUntil (cond, lock, limit) andalso check ();
       val ok = restore_attributes check ()
-        handle Interrupt => (Mutex.unlock lock; raise Interrupt);
+        handle Exn.Interrupt => (Mutex.unlock lock; raise Exn.Interrupt);
       val res = if ok then SOME (change_result messages Queue.dequeue) else NONE;
 
       val _ = Mutex.unlock lock;
diff -r bd9573735bdd -r de653f1ad78b src/Pure/Concurrent/par_list.ML
--- a/src/Pure/Concurrent/par_list.ML	Wed Oct 01 12:00:01 2008 +0200
+++ b/src/Pure/Concurrent/par_list.ML	Wed Oct 01 12:00:02 2008 +0200
@@ -32,7 +32,7 @@
     Future.join_results (List.map (fn x => Future.future (SOME group) [] true (fn () => f x)) xs)
   end;
 
-fun map f xs = Future.release_results (raw_map f xs);
+fun map f xs = Exn.release_first (raw_map f xs);
 
 fun get_some f xs =
   let
@@ -43,7 +43,7 @@
   in
     (case get_first found results of
       SOME y => SOME y
-    | NONE => (Future.release_results results; NONE))
+    | NONE => (Exn.release_first results; NONE))
   end;
 
 fun find_some P = get_some (fn x => if P x then SOME x else NONE);
diff -r bd9573735bdd -r de653f1ad78b src/Pure/General/basics.ML
--- a/src/Pure/General/basics.ML	Wed Oct 01 12:00:01 2008 +0200
+++ b/src/Pure/General/basics.ML	Wed Oct 01 12:00:02 2008 +0200
@@ -95,7 +95,7 @@
 (* partiality *)
 
 fun try f x = SOME (f x)
-  handle Interrupt => raise Interrupt | _ => NONE;
+  handle Exn.Interrupt => raise Exn.Interrupt | _ => NONE;
 
 fun can f x = is_some (try f x);
 
diff -r bd9573735bdd -r de653f1ad78b src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Oct 01 12:00:01 2008 +0200
+++ b/src/Pure/Isar/proof.ML	Wed Oct 01 12:00:02 2008 +0200
@@ -962,7 +962,7 @@
       (case test_proof goal_state of
         Exn.Result (SOME _) => goal_state
       | Exn.Result NONE => error (fail_msg (context_of goal_state))
-      | Exn.Exn Interrupt => raise Interrupt
+      | Exn.Exn Exn.Interrupt => raise Exn.Interrupt
       | Exn.Exn exn => raise Exn.EXCEPTIONS ([exn], fail_msg (context_of goal_state))))
   end;
 
diff -r bd9573735bdd -r de653f1ad78b src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed Oct 01 12:00:01 2008 +0200
+++ b/src/Pure/Isar/toplevel.ML	Wed Oct 01 12:00:02 2008 +0200
@@ -263,7 +263,7 @@
       | exn_msg ctxt (EXCURSION_FAIL (exn, loc)) =
           exn_msg ctxt exn ^ Markup.markup Markup.location ("\n" ^ loc)
       | exn_msg _ TERMINATE = "Exit."
-      | exn_msg _ Interrupt = "Interrupt."
+      | exn_msg _ Exn.Interrupt = "Interrupt."
       | exn_msg _ TimeLimit.TimeOut = "Timeout."
       | exn_msg _ TOPLEVEL_ERROR = "Error."
       | exn_msg _ (SYS_ERROR msg) = "## SYSTEM ERROR ##\n" ^ msg
diff -r bd9573735bdd -r de653f1ad78b src/Pure/ML-Systems/mosml.ML
--- a/src/Pure/ML-Systems/mosml.ML	Wed Oct 01 12:00:01 2008 +0200
+++ b/src/Pure/ML-Systems/mosml.ML	Wed Oct 01 12:00:02 2008 +0200
@@ -36,6 +36,8 @@
 load "FileSys";
 load "IO";
 
+exception Interrupt;
+
 use "ML-Systems/exn.ML";
 use "ML-Systems/universal.ML";
 use "ML-Systems/multithreading.ML";
@@ -178,8 +180,6 @@
 
 (* FIXME proper implementation available? *)
 
-exception Interrupt;
-
 fun interruptible f x = f x;
 fun uninterruptible f x = f (fn (g: 'c -> 'd) => g) x;
 
diff -r bd9573735bdd -r de653f1ad78b src/Pure/ML-Systems/multithreading_polyml.ML
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Wed Oct 01 12:00:01 2008 +0200
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Wed Oct 01 12:00:02 2008 +0200
@@ -80,7 +80,7 @@
         val result = Exn.capture (f orig_atts) x;
         val _ = restore ();
       in result end
-      handle Interrupt => (restore (); Exn.Exn Interrupt))
+      handle Exn.Interrupt => (restore (); Exn.Exn Exn.Interrupt))
   end;
 
 fun interruptible f = with_attributes regular_interrupts (fn _ => f);
@@ -105,7 +105,7 @@
 
     (*RACE! timeout signal vs. external Interrupt*)
     val result = Exn.capture (restore_attributes f) x;
-    val was_timeout = (case result of Exn.Exn Interrupt => ! timeout | _ => false);
+    val was_timeout = (case result of Exn.Exn Exn.Interrupt => ! timeout | _ => false);
 
     val _ = Thread.interrupt watchdog handle Thread _ => ();
   in if was_timeout then raise TimeOut else Exn.release result end) ();
@@ -165,7 +165,7 @@
     val _ = while ! result = Wait do
       restore_attributes (fn () =>
         (ConditionVar.waitUntil (result_cond, result_mutex, Time.now () + Time.fromMilliseconds 100); ())
-          handle Interrupt => kill 10) ();
+          handle Exn.Interrupt => kill 10) ();
 
     (*cleanup*)
     val output = read_file output_name handle IO.Io _ => "";
@@ -173,7 +173,7 @@
     val _ = OS.FileSys.remove pid_name handle OS.SysErr _ => ();
     val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
     val _ = Thread.interrupt system_thread handle Thread _ => ();
-    val rc = (case ! result of Signal => raise Interrupt | Result rc => rc);
+    val rc = (case ! result of Signal => raise Exn.Interrupt | Result rc => rc);
   in (output, rc) end) ();
 
 
diff -r bd9573735bdd -r de653f1ad78b src/Pure/ML-Systems/polyml_common.ML
--- a/src/Pure/ML-Systems/polyml_common.ML	Wed Oct 01 12:00:01 2008 +0200
+++ b/src/Pure/ML-Systems/polyml_common.ML	Wed Oct 01 12:00:02 2008 +0200
@@ -4,6 +4,8 @@
 Compatibility file for Poly/ML -- common part for 4.x and 5.x.
 *)
 
+exception Interrupt = SML90.Interrupt;
+
 use "ML-Systems/exn.ML";
 use "ML-Systems/multithreading.ML";
 use "ML-Systems/time_limit.ML";
@@ -93,8 +95,6 @@
 
 (** interrupts **)
 
-exception Interrupt = SML90.Interrupt;
-
 local
 
 val sig_int = 2;
diff -r bd9573735bdd -r de653f1ad78b src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/smlnj.ML	Wed Oct 01 12:00:01 2008 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Wed Oct 01 12:00:02 2008 +0200
@@ -4,6 +4,8 @@
 Compatibility file for Standard ML of New Jersey 110 or later.
 *)
 
+exception Interrupt;
+
 use "ML-Systems/proper_int.ML";
 use "ML-Systems/overloading_smlnj.ML";
 use "ML-Systems/exn.ML";
@@ -145,8 +147,6 @@
 
 (** interrupts **)
 
-exception Interrupt;
-
 local
 
 fun change_signal new_handler f x =
diff -r bd9573735bdd -r de653f1ad78b src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Wed Oct 01 12:00:01 2008 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Wed Oct 01 12:00:02 2008 +0200
@@ -999,7 +999,7 @@
     case (e,srco) of
         (XML_PARSE,SOME src) =>
         panic "Invalid XML input, aborting" (* TODO: attempt recovery  *)
-      | (Interrupt,SOME src) =>
+      | (Exn.Interrupt,SOME src) =>
         (Output.error_msg "Interrupt during PGIP processing"; loop true src)
       | (Toplevel.UNDEF,SOME src) =>
         (Output.error_msg "No working context defined"; loop true src)