# HG changeset patch
# User blanchet
# Date 1289132999 -3600
# Node ID 36b7ed41ca9ff36a30b5efc9a44a6f47ac73faa0
# Parent  8adcdd2c5805faaa5421a08841196ae98cae78f0
removed explicit "Interrupt" handling for conformity with async model -- unfortunately the user loses the information about how many scopes were checked, but this needs to be retought with the new interface anyway

diff -r 8adcdd2c5805 -r 36b7ed41ca9f src/HOL/Tools/Nitpick/kodkod.ML
--- a/src/HOL/Tools/Nitpick/kodkod.ML	Sat Nov 06 10:25:08 2010 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.ML	Sun Nov 07 13:29:59 2010 +0100
@@ -160,7 +160,6 @@
     KodkodiNotInstalled |
     Normal of (int * raw_bound list) list * int list * string |
     TimedOut of int list |
-    Interrupted of int list option |
     Error of string * int list
 
   exception SYNTAX of string * string
@@ -308,7 +307,6 @@
   KodkodiNotInstalled |
   Normal of (int * raw_bound list) list * int list * string |
   TimedOut of int list |
-  Interrupted of int list option |
   Error of string * int list
 
 exception SYNTAX of string * string
@@ -1085,17 +1083,6 @@
                 Normal (ps, js, first_error)
             end
         in remove_temporary_files (); outcome end
-        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)))  (* FIXME violates Isabelle/ML exception model *)
-                 handle Exn.Interrupt =>  (* FIXME violates Isabelle/ML exception model *)
-                        (remove_temporary_files (); Interrupted NONE)
-               end
       end
   end
 
diff -r 8adcdd2c5805 -r 36b7ed41ca9f src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Sat Nov 06 10:25:08 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Sun Nov 07 13:29:59 2010 +0100
@@ -231,9 +231,6 @@
     fun check_deadline () =
       if debug andalso passed_deadline deadline then raise TimeLimit.TimeOut
       else ()
-    fun do_interrupted () =
-      if passed_deadline deadline then raise TimeLimit.TimeOut
-      else raise Interrupt
 
     val assm_ts = if assms orelse auto then assm_ts else []
     val _ =
@@ -818,9 +815,6 @@
             end
           | KK.TimedOut unsat_js =>
             (update_checked_problems problems unsat_js; raise TimeLimit.TimeOut)
-          | KK.Interrupted NONE => (checked_problems := NONE; do_interrupted ())
-          | KK.Interrupted (SOME unsat_js) =>
-            (update_checked_problems problems unsat_js; do_interrupted ())
           | KK.Error (s, unsat_js) =>
             (update_checked_problems problems unsat_js;
              print_v (K ("Kodkod error: " ^ s ^ "."));
@@ -971,27 +965,15 @@
 
     val batches = batch_list batch_size (!scopes)
     val outcome_code =
-      (run_batches 0 (length batches) batches
-                   (false, max_potential, max_genuine, 0)
-       handle Exn.Interrupt => do_interrupted ())  (* FIXME violates Isabelle/ML exception model *)
+      run_batches 0 (length batches) batches
+                  (false, max_potential, max_genuine, 0)
       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")  (* 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 =>  (* 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."  (* 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 =