# HG changeset patch
# User blanchet
# Date 1256851890 -3600
# Node ID 118517551c1269b25f5cb9b7dfb99e650334b449
# Parent  113e235e84e3f4b35cfd3bd277f74fb9197a167b
try very hard to remove temporary files generated by Nitpick in case of interruption

diff -r 113e235e84e3 -r 118517551c12 src/HOL/Tools/Nitpick/kodkod.ML
--- a/src/HOL/Tools/Nitpick/kodkod.ML	Thu Oct 29 21:57:59 2009 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.ML	Thu Oct 29 22:31:30 2009 +0100
@@ -1027,12 +1027,10 @@
         val err_path = path_for "kodkodi" "err"
         val _ = write_problem_file out (map snd indexed_problems)
         val _ = File.write_buffer in_path (!in_buf)
-        (* (int list -> outcome) -> outcome *)
-        fun stopped constr =
-          let val nontriv_js = map reindex (snd (read_output_file out_path)) in
-            constr (triv_js @ nontriv_js)
-            handle Exn.Interrupt => Interrupted NONE
-          end
+        (* unit -> unit *)
+        fun remove_temporary_files () =
+          if overlord then ()
+          else List.app File.rm [in_path, out_path, err_path]
       in
         let
           val ms =
@@ -1085,12 +1083,16 @@
               else
                 Normal (ps, js)
             end
-        in
-          if overlord then ()
-          else List.app File.rm [in_path, out_path, err_path];
-          outcome
-        end
-        handle Exn.Interrupt => stopped (Interrupted o SOME)
+        in remove_temporary_files (); outcome end
+        handle Exn.Interrupt =>
+               let
+                 val nontriv_js = map reindex (snd (read_output_file out_path))
+               in
+                 (remove_temporary_files ();
+                  Interrupted (SOME (triv_js @ nontriv_js)))
+                 handle Exn.Interrupt =>
+                        (remove_temporary_files (); Interrupted NONE)
+               end
       end
   end