# HG changeset patch
# User blanchet
# Date 1284041171 -7200
# Node ID bdfcf243460190dd9adaa7acfb52ef0af16e99b4
# Parent  b1bfb3de88fdd3b64c3f4221884a77c971e7b009
better error reporting when the Sledgehammer minimizer is interrupted

diff -r b1bfb3de88fd -r bdfcf2434601 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Thu Sep 09 14:47:06 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu Sep 09 16:06:11 2010 +0200
@@ -10,7 +10,7 @@
   datatype failure =
     Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
     OutOfResources | SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl |
-    MalformedInput | MalformedOutput | UnknownError
+    MalformedInput | MalformedOutput | Interrupted | UnknownError
 
   type prover_config =
     {exec: string * string,
@@ -42,7 +42,7 @@
 datatype failure =
   Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
   SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl | MalformedInput |
-  MalformedOutput | UnknownError
+  MalformedOutput | Interrupted | UnknownError
 
 type prover_config =
   {exec: string * string,
@@ -85,6 +85,7 @@
     "The ATP problem is malformed. Please report this to the Isabelle \
     \developers."
   | string_for_failure MalformedOutput = "The ATP output is malformed."
+  | string_for_failure Interrupted = "The ATP was interrupted."
   | string_for_failure UnknownError = "An unknown ATP error occurred."
 
 fun known_failure_in_output output =
diff -r b1bfb3de88fd -r bdfcf2434601 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Sep 09 14:47:06 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Sep 09 16:06:11 2010 +0200
@@ -162,7 +162,10 @@
                               output =
   case known_failure_in_output output known_failures of
     NONE => (case extract_proof proof_delims output of
-             "" => ("", SOME MalformedOutput)
+             "" => ("", SOME (if res_code = 0 andalso output = "" then
+                                Interrupted
+                              else
+                                UnknownError))
            | proof => if res_code = 0 then (proof, NONE)
                       else ("", SOME UnknownError))
   | SOME failure =>
diff -r b1bfb3de88fd -r bdfcf2434601 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Sep 09 14:47:06 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Sep 09 16:06:11 2010 +0200
@@ -31,6 +31,7 @@
 
 fun string_for_failure Unprovable = "Unprovable."
   | string_for_failure TimedOut = "Timed out."
+  | string_for_failure Interrupted = "Interrupted."
   | string_for_failure _ = "Unknown error."
 
 fun n_theorems names =