explicit indication of some remaining violations of the Isabelle/ML interrupt model;

--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Nov 05 19:39:25 2010 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Nov 05 19:47:20 2010 +0100
@@ -179,7 +179,7 @@
          | Refute.REFUTE (loc, details) =>
            (error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^
                    "."))
-         | Exn.Interrupt => raise Exn.Interrupt
+         | Exn.Interrupt => raise Exn.Interrupt  (* FIXME violates Isabelle/ML exception model *)
          | _ => (Output.urgent_message ("Unknown error in Nitpick"); Error)
   end
 val nitpick_mtd = ("nitpick", invoke_nitpick)

--- a/src/HOL/Tools/Nitpick/kodkod.ML	Fri Nov 05 19:39:25 2010 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.ML	Fri Nov 05 19:47:20 2010 +0100
@@ -1085,15 +1085,15 @@
                 Normal (ps, js, first_error)
             end
         in remove_temporary_files (); outcome end
-        handle Exn.Interrupt =>
+        handle Exn.Interrupt =>  (* FIXME Exn.is_interrupt *)
                let
                  val nontriv_js =
                    read_output_file new_kodkodi out_path
                    |> snd |> snd |> map reindex
                in
                  (remove_temporary_files ();
-                  Interrupted (SOME (triv_js @ nontriv_js)))
-                 handle Exn.Interrupt =>
+                  Interrupted (SOME (triv_js @ nontriv_js)))  (* FIXME violates Isabelle/ML exception model *)
+                 handle Exn.Interrupt =>  (* FIXME violates Isabelle/ML exception model *)
                         (remove_temporary_files (); Interrupted NONE)
                end
       end

--- a/src/HOL/Tools/Nitpick/nitpick.ML	Fri Nov 05 19:39:25 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Fri Nov 05 19:47:20 2010 +0100
@@ -973,25 +973,25 @@
     val outcome_code =
       (run_batches 0 (length batches) batches
                    (false, max_potential, max_genuine, 0)
-       handle Exn.Interrupt => do_interrupted ())
+       handle Exn.Interrupt => do_interrupted ())  (* FIXME violates Isabelle/ML exception model *)
       handle TimeLimit.TimeOut =>
              (print_m (fn () => excipit "ran out of time after checking");
               if !met_potential > 0 then "potential" else "unknown")
            | Exn.Interrupt =>
              if auto orelse debug then raise Interrupt
-             else error (excipit "was interrupted after checking")
+             else error (excipit "was interrupted after checking")  (* FIXME violates Isabelle/ML exception model *)
     val _ = print_v (fn () =>
                 "Total time: " ^ string_from_time (Timer.checkRealTimer timer) ^
                 ".")
   in (outcome_code, !state_ref) end
-  handle Exn.Interrupt =>
+  handle Exn.Interrupt =>  (* FIXME violates Isabelle/ML exception model *)
          if auto orelse #debug params then
            raise Interrupt
          else
            if passed_deadline deadline then
              (Output.urgent_message "Nitpick ran out of time."; ("unknown", state))
            else
-             error "Nitpick was interrupted."
+             error "Nitpick was interrupted."  (* FIXME violates Isabelle/ML exception model *)
 
 fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) auto i n
                       step subst assm_ts orig_t =

--- a/src/Tools/quickcheck.ML	Fri Nov 05 19:39:25 2010 +0100
+++ b/src/Tools/quickcheck.ML	Fri Nov 05 19:47:20 2010 +0100
@@ -239,7 +239,7 @@
         | SOME ts => SOME (names ~~ ts)) (with_size 1 []))) ()
       handle TimeLimit.TimeOut =>
         error (excipit "ran out of time")
-     | Exn.Interrupt => error (excipit "was interrupted")
+     | Exn.Interrupt => error (excipit "was interrupted")  (* FIXME violates Isabelle/ML exception model *)
   in
     (result, ([exec_time, comp_time], if report ctxt then SOME reports else NONE))
   end;