# HG changeset patch
# User blanchet
# Date 1297328978 -3600
# Node ID a18e7bbca258be6c697de74de1ef379702735067
# Parent  d52af5722f0f1686d619ba024d41f7d04f4189ec
make minimizer verbose

diff -r d52af5722f0f -r a18e7bbca258 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Wed Feb 09 17:18:58 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Thu Feb 10 10:09:38 2011 +0100
@@ -27,7 +27,7 @@
 
   val strip_spaces : (char -> bool) -> string -> string
   val short_output : bool -> string -> string
-  val string_for_failure : string -> failure -> string
+  val string_for_failure : failure -> string
   val extract_important_message : string -> string
   val extract_known_failure :
     (failure * string) list -> string -> failure option
@@ -82,22 +82,20 @@
 fun short_output verbose output =
   if verbose then elide_string 1000 output else ""
 
-fun missing_message_tail prover =
-  " appears to be missing. You will need to install it if you want to run " ^
-  prover ^ "s remotely."
+val missing_message_tail =
+  " appears to be missing. You will need to install it if you want to invoke \
+  \remote provers."
 
-fun string_for_failure prover Unprovable =
-    "The " ^ prover ^ " problem is unprovable."
-  | string_for_failure prover IncompleteUnprovable =
-    "The " ^ prover ^ " cannot prove the problem."
-  | string_for_failure prover ProofMissing =
-    "The " ^ prover ^ " claims the conjecture is a theorem but did not provide \
-    \a proof."
-  | string_for_failure _ CantConnect = "Cannot connect to remote server."
-  | string_for_failure _ TimedOut = "Timed out."
-  | string_for_failure prover OutOfResources =
-    "The " ^ prover ^ " ran out of resources."
-  | string_for_failure _ SpassTooOld =
+fun string_for_failure Unprovable =
+    "The problem is unprovable."
+  | string_for_failure IncompleteUnprovable =
+    "The prover gave up."
+  | string_for_failure ProofMissing =
+    "The prover claims the conjecture is a theorem but did not provide a proof."
+  | string_for_failure CantConnect = "Cannot connect to remote server."
+  | string_for_failure TimedOut = "Timed out."
+  | string_for_failure OutOfResources = "The prover ran out of resources."
+  | string_for_failure SpassTooOld =
     "Isabelle requires a more recent version of SPASS with support for the \
     \TPTP syntax. To install it, download and extract the package \
     \\"http://isabelle.in.tum.de/dist/contrib/spass-3.7.tar.gz\" and add the \
@@ -106,26 +104,23 @@
                (Path.variable "ISABELLE_HOME_USER" ::
                 map Path.basic ["etc", "components"])))) ^
     " on a line of its own."
-  | string_for_failure _ VampireTooOld =
+  | string_for_failure VampireTooOld =
     "Isabelle requires a more recent version of Vampire. To install it, follow \
     \the instructions from the Sledgehammer manual (\"isabelle doc\
     \ sledgehammer\")."
-  | string_for_failure prover NoPerl = "Perl" ^ missing_message_tail prover
-  | string_for_failure prover NoLibwwwPerl =
-    "The Perl module \"libwww-perl\"" ^ missing_message_tail prover
-  | string_for_failure _ NoRealZ3 =
+  | string_for_failure NoPerl = "Perl" ^ missing_message_tail
+  | string_for_failure NoLibwwwPerl =
+    "The Perl module \"libwww-perl\"" ^ missing_message_tail
+  | string_for_failure NoRealZ3 =
     "The environment variable \"Z3_REAL_SOLVER\" must be set to Z3's full path."
-  | string_for_failure prover MalformedInput =
-    "The " ^ prover ^ " problem is malformed. Please report this to the \
-    \Isabelle developers."
-  | string_for_failure prover MalformedOutput =
-    "The " ^ prover ^ " output is malformed."
-  | string_for_failure prover Crashed = "The " ^ prover ^ " crashed."
-  | string_for_failure prover InternalError =
-    "An internal " ^ prover ^ " error occurred."
-  | string_for_failure prover (UnknownError string) =
-    (* "An" is correct for "ATP" and "SMT". *)
-    "An " ^ prover ^ " error occurred" ^
+  | string_for_failure MalformedInput =
+    "The generated problem is malformed. Please report this to the Isabelle \
+    \developers."
+  | string_for_failure MalformedOutput = "The prover output is malformed."
+  | string_for_failure Crashed = "The prover crashed."
+  | string_for_failure InternalError = "An internal prover error occurred."
+  | string_for_failure (UnknownError string) =
+    "A prover error occurred" ^
     (if string = "" then ". (Pass the \"verbose\" option for details.)"
      else ":\n" ^ string)
 
diff -r d52af5722f0f -r a18e7bbca258 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Wed Feb 09 17:18:58 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu Feb 10 10:09:38 2011 +0100
@@ -260,7 +260,7 @@
     (output, 0) => split_lines output
   | (output, _) =>
     error (case extract_known_failure known_perl_failures output of
-             SOME failure => string_for_failure "ATP" failure
+             SOME failure => string_for_failure failure
            | NONE => perhaps (try (unsuffix "\n")) output ^ ".")
 
 fun find_system name [] systems = find_first (String.isPrefix name) systems
diff -r d52af5722f0f -r a18e7bbca258 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Feb 09 17:18:58 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Feb 10 10:09:38 2011 +0100
@@ -81,7 +81,9 @@
   in
     print silent (fn () =>
         case outcome of
-          SOME failure => short_string_for_failure failure
+          SOME failure =>
+          (if verbose then string_for_failure else short_string_for_failure)
+              failure
         | NONE =>
           if length used_facts = length facts then "Found proof."
           else "Found proof with " ^ n_facts used_facts ^ ".");
diff -r d52af5722f0f -r a18e7bbca258 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Feb 09 17:18:58 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Feb 10 10:09:38 2011 +0100
@@ -467,7 +467,7 @@
                |>> append_to_message)
       | SOME ProofMissing =>
         (NONE, metis_proof_text metis_params |>> append_to_message)
-      | SOME failure => (outcome, (string_for_failure "ATP" failure, []))
+      | SOME failure => (outcome, (string_for_failure failure, []))
   in
     {outcome = outcome, message = message, used_facts = used_facts,
      run_time_in_msecs = msecs}
@@ -663,7 +663,7 @@
            else
              "")
         end
-      | SOME failure => string_for_failure "SMT solver" failure
+      | SOME failure => string_for_failure failure
   in
     {outcome = outcome, used_facts = map fst used_facts,
      run_time_in_msecs = run_time_in_msecs, message = message}