more robust treatment of Interrupt (cf. exn.ML);
authorwenzelm
Wed Oct 01 12:00:02 2008 +0200 (2008-10-01 ago)
changeset 28443de653f1ad78b
parent 28442 bd9573735bdd
child 28444 283d5e41953d
more robust treatment of Interrupt (cf. exn.ML);
src/Pure/Concurrent/mailbox.ML
src/Pure/Concurrent/par_list.ML
src/Pure/General/basics.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/toplevel.ML
src/Pure/ML-Systems/mosml.ML
src/Pure/ML-Systems/multithreading_polyml.ML
src/Pure/ML-Systems/polyml_common.ML
src/Pure/ML-Systems/smlnj.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
     1.1 --- a/src/Pure/Concurrent/mailbox.ML	Wed Oct 01 12:00:01 2008 +0200
     1.2 +++ b/src/Pure/Concurrent/mailbox.ML	Wed Oct 01 12:00:02 2008 +0200
     1.3 @@ -52,7 +52,7 @@
     1.4        fun check () = not (Queue.is_empty (! messages)) orelse
     1.5          ConditionVar.waitUntil (cond, lock, limit) andalso check ();
     1.6        val ok = restore_attributes check ()
     1.7 -        handle Interrupt => (Mutex.unlock lock; raise Interrupt);
     1.8 +        handle Exn.Interrupt => (Mutex.unlock lock; raise Exn.Interrupt);
     1.9        val res = if ok then SOME (change_result messages Queue.dequeue) else NONE;
    1.10  
    1.11        val _ = Mutex.unlock lock;
     2.1 --- a/src/Pure/Concurrent/par_list.ML	Wed Oct 01 12:00:01 2008 +0200
     2.2 +++ b/src/Pure/Concurrent/par_list.ML	Wed Oct 01 12:00:02 2008 +0200
     2.3 @@ -32,7 +32,7 @@
     2.4      Future.join_results (List.map (fn x => Future.future (SOME group) [] true (fn () => f x)) xs)
     2.5    end;
     2.6  
     2.7 -fun map f xs = Future.release_results (raw_map f xs);
     2.8 +fun map f xs = Exn.release_first (raw_map f xs);
     2.9  
    2.10  fun get_some f xs =
    2.11    let
    2.12 @@ -43,7 +43,7 @@
    2.13    in
    2.14      (case get_first found results of
    2.15        SOME y => SOME y
    2.16 -    | NONE => (Future.release_results results; NONE))
    2.17 +    | NONE => (Exn.release_first results; NONE))
    2.18    end;
    2.19  
    2.20  fun find_some P = get_some (fn x => if P x then SOME x else NONE);
     3.1 --- a/src/Pure/General/basics.ML	Wed Oct 01 12:00:01 2008 +0200
     3.2 +++ b/src/Pure/General/basics.ML	Wed Oct 01 12:00:02 2008 +0200
     3.3 @@ -95,7 +95,7 @@
     3.4  (* partiality *)
     3.5  
     3.6  fun try f x = SOME (f x)
     3.7 -  handle Interrupt => raise Interrupt | _ => NONE;
     3.8 +  handle Exn.Interrupt => raise Exn.Interrupt | _ => NONE;
     3.9  
    3.10  fun can f x = is_some (try f x);
    3.11  
     4.1 --- a/src/Pure/Isar/proof.ML	Wed Oct 01 12:00:01 2008 +0200
     4.2 +++ b/src/Pure/Isar/proof.ML	Wed Oct 01 12:00:02 2008 +0200
     4.3 @@ -962,7 +962,7 @@
     4.4        (case test_proof goal_state of
     4.5          Exn.Result (SOME _) => goal_state
     4.6        | Exn.Result NONE => error (fail_msg (context_of goal_state))
     4.7 -      | Exn.Exn Interrupt => raise Interrupt
     4.8 +      | Exn.Exn Exn.Interrupt => raise Exn.Interrupt
     4.9        | Exn.Exn exn => raise Exn.EXCEPTIONS ([exn], fail_msg (context_of goal_state))))
    4.10    end;
    4.11  
     5.1 --- a/src/Pure/Isar/toplevel.ML	Wed Oct 01 12:00:01 2008 +0200
     5.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Oct 01 12:00:02 2008 +0200
     5.3 @@ -263,7 +263,7 @@
     5.4        | exn_msg ctxt (EXCURSION_FAIL (exn, loc)) =
     5.5            exn_msg ctxt exn ^ Markup.markup Markup.location ("\n" ^ loc)
     5.6        | exn_msg _ TERMINATE = "Exit."
     5.7 -      | exn_msg _ Interrupt = "Interrupt."
     5.8 +      | exn_msg _ Exn.Interrupt = "Interrupt."
     5.9        | exn_msg _ TimeLimit.TimeOut = "Timeout."
    5.10        | exn_msg _ TOPLEVEL_ERROR = "Error."
    5.11        | exn_msg _ (SYS_ERROR msg) = "## SYSTEM ERROR ##\n" ^ msg
     6.1 --- a/src/Pure/ML-Systems/mosml.ML	Wed Oct 01 12:00:01 2008 +0200
     6.2 +++ b/src/Pure/ML-Systems/mosml.ML	Wed Oct 01 12:00:02 2008 +0200
     6.3 @@ -36,6 +36,8 @@
     6.4  load "FileSys";
     6.5  load "IO";
     6.6  
     6.7 +exception Interrupt;
     6.8 +
     6.9  use "ML-Systems/exn.ML";
    6.10  use "ML-Systems/universal.ML";
    6.11  use "ML-Systems/multithreading.ML";
    6.12 @@ -178,8 +180,6 @@
    6.13  
    6.14  (* FIXME proper implementation available? *)
    6.15  
    6.16 -exception Interrupt;
    6.17 -
    6.18  fun interruptible f x = f x;
    6.19  fun uninterruptible f x = f (fn (g: 'c -> 'd) => g) x;
    6.20  
     7.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Wed Oct 01 12:00:01 2008 +0200
     7.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Wed Oct 01 12:00:02 2008 +0200
     7.3 @@ -80,7 +80,7 @@
     7.4          val result = Exn.capture (f orig_atts) x;
     7.5          val _ = restore ();
     7.6        in result end
     7.7 -      handle Interrupt => (restore (); Exn.Exn Interrupt))
     7.8 +      handle Exn.Interrupt => (restore (); Exn.Exn Exn.Interrupt))
     7.9    end;
    7.10  
    7.11  fun interruptible f = with_attributes regular_interrupts (fn _ => f);
    7.12 @@ -105,7 +105,7 @@
    7.13  
    7.14      (*RACE! timeout signal vs. external Interrupt*)
    7.15      val result = Exn.capture (restore_attributes f) x;
    7.16 -    val was_timeout = (case result of Exn.Exn Interrupt => ! timeout | _ => false);
    7.17 +    val was_timeout = (case result of Exn.Exn Exn.Interrupt => ! timeout | _ => false);
    7.18  
    7.19      val _ = Thread.interrupt watchdog handle Thread _ => ();
    7.20    in if was_timeout then raise TimeOut else Exn.release result end) ();
    7.21 @@ -165,7 +165,7 @@
    7.22      val _ = while ! result = Wait do
    7.23        restore_attributes (fn () =>
    7.24          (ConditionVar.waitUntil (result_cond, result_mutex, Time.now () + Time.fromMilliseconds 100); ())
    7.25 -          handle Interrupt => kill 10) ();
    7.26 +          handle Exn.Interrupt => kill 10) ();
    7.27  
    7.28      (*cleanup*)
    7.29      val output = read_file output_name handle IO.Io _ => "";
    7.30 @@ -173,7 +173,7 @@
    7.31      val _ = OS.FileSys.remove pid_name handle OS.SysErr _ => ();
    7.32      val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
    7.33      val _ = Thread.interrupt system_thread handle Thread _ => ();
    7.34 -    val rc = (case ! result of Signal => raise Interrupt | Result rc => rc);
    7.35 +    val rc = (case ! result of Signal => raise Exn.Interrupt | Result rc => rc);
    7.36    in (output, rc) end) ();
    7.37  
    7.38  
     8.1 --- a/src/Pure/ML-Systems/polyml_common.ML	Wed Oct 01 12:00:01 2008 +0200
     8.2 +++ b/src/Pure/ML-Systems/polyml_common.ML	Wed Oct 01 12:00:02 2008 +0200
     8.3 @@ -4,6 +4,8 @@
     8.4  Compatibility file for Poly/ML -- common part for 4.x and 5.x.
     8.5  *)
     8.6  
     8.7 +exception Interrupt = SML90.Interrupt;
     8.8 +
     8.9  use "ML-Systems/exn.ML";
    8.10  use "ML-Systems/multithreading.ML";
    8.11  use "ML-Systems/time_limit.ML";
    8.12 @@ -93,8 +95,6 @@
    8.13  
    8.14  (** interrupts **)
    8.15  
    8.16 -exception Interrupt = SML90.Interrupt;
    8.17 -
    8.18  local
    8.19  
    8.20  val sig_int = 2;
     9.1 --- a/src/Pure/ML-Systems/smlnj.ML	Wed Oct 01 12:00:01 2008 +0200
     9.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Wed Oct 01 12:00:02 2008 +0200
     9.3 @@ -4,6 +4,8 @@
     9.4  Compatibility file for Standard ML of New Jersey 110 or later.
     9.5  *)
     9.6  
     9.7 +exception Interrupt;
     9.8 +
     9.9  use "ML-Systems/proper_int.ML";
    9.10  use "ML-Systems/overloading_smlnj.ML";
    9.11  use "ML-Systems/exn.ML";
    9.12 @@ -145,8 +147,6 @@
    9.13  
    9.14  (** interrupts **)
    9.15  
    9.16 -exception Interrupt;
    9.17 -
    9.18  local
    9.19  
    9.20  fun change_signal new_handler f x =
    10.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Wed Oct 01 12:00:01 2008 +0200
    10.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Wed Oct 01 12:00:02 2008 +0200
    10.3 @@ -999,7 +999,7 @@
    10.4      case (e,srco) of
    10.5          (XML_PARSE,SOME src) =>
    10.6          panic "Invalid XML input, aborting" (* TODO: attempt recovery  *)
    10.7 -      | (Interrupt,SOME src) =>
    10.8 +      | (Exn.Interrupt,SOME src) =>
    10.9          (Output.error_msg "Interrupt during PGIP processing"; loop true src)
   10.10        | (Toplevel.UNDEF,SOME src) =>
   10.11          (Output.error_msg "No working context defined"; loop true src)