more precise error messages in "verbose" (or "debug") mode, following this morning's permission debacle

--- a/src/HOL/Tools/ATP/atp_proof.ML	Fri Dec 17 21:47:13 2010 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Fri Dec 17 22:15:08 2010 +0100
@@ -15,7 +15,7 @@
     Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
     OutOfResources | SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl |
     NoRealZ3 | MalformedInput | MalformedOutput | Interrupted | Crashed |
-    InternalError | UnknownError
+    InternalError | UnknownError of string
 
   type step_name = string * string option
 
@@ -26,13 +26,14 @@
   type 'a proof = 'a uniform_formula step list
 
   val strip_spaces : (char -> bool) -> string -> string
+  val short_output : bool -> string -> string
   val string_for_failure : string -> failure -> string
   val extract_important_message : string -> string
   val extract_known_failure :
     (failure * string) list -> string -> failure option
   val extract_tstplike_proof_and_outcome :
-    bool -> int -> (string * string) list -> (failure * string) list -> string
-    -> string * failure option
+    bool -> bool -> int -> (string * string) list -> (failure * string) list
+    -> string -> string * failure option
   val is_same_step : step_name * step_name -> bool
   val atp_proof_from_tstplike_string : bool -> string -> string proof
   val map_term_names_in_atp_proof :
@@ -49,7 +50,7 @@
   Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
   SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl | NoRealZ3 |
   MalformedInput | MalformedOutput | Interrupted | Crashed | InternalError |
-  UnknownError
+  UnknownError of string
 
 fun strip_spaces_in_list _ [] = []
   | strip_spaces_in_list _ [c1] = if Char.isSpace c1 then [] else [str c1]
@@ -72,6 +73,15 @@
 fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
 val strip_spaces_except_between_ident_chars = strip_spaces is_ident_char
 
+fun elide_string threshold s =
+  if size s > threshold then
+    String.extract (s, 0, SOME (threshold div 2 - 5)) ^ " ...... " ^
+    String.extract (s, size s - (threshold + 1) div 2 + 6, NONE)
+  else
+    s
+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."
@@ -112,9 +122,10 @@
   | string_for_failure prover Crashed = "The " ^ prover ^ " crashed."
   | string_for_failure prover InternalError =
     "An internal " ^ prover ^ " error occurred."
-  | string_for_failure prover UnknownError =
+  | string_for_failure prover (UnknownError string) =
     (* "An" is correct for "ATP" and "SMT". *)
-    "An " ^ prover ^ " error occurred."
+    "An " ^ prover ^ " error occurred" ^
+    (if string = "" then "." else ":\n" ^ string)
 
 fun extract_delimited (begin_delim, end_delim) output =
   output |> first_field begin_delim |> the |> snd
@@ -146,16 +157,17 @@
   |> find_first (fn (_, pattern) => String.isSubstring pattern output)
   |> Option.map fst
 
-fun extract_tstplike_proof_and_outcome complete res_code proof_delims
+fun extract_tstplike_proof_and_outcome verbose complete res_code proof_delims
                                        known_failures output =
   case extract_known_failure known_failures output of
     NONE => (case extract_tstplike_proof proof_delims output of
              "" => ("", SOME (if res_code = 0 andalso output = "" then
                                 Interrupted
                               else
-                                UnknownError))
-           | tstplike_proof => if res_code = 0 then (tstplike_proof, NONE)
-                               else ("", SOME UnknownError))
+                                UnknownError (short_output verbose output)))
+           | tstplike_proof =>
+             if res_code = 0 then (tstplike_proof, NONE)
+             else ("", SOME (UnknownError (short_output verbose output))))
   | SOME failure =>
     ("", SOME (if failure = IncompleteUnprovable andalso complete then
                  Unprovable

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Dec 17 21:47:13 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Dec 17 22:15:08 2010 +0100
@@ -167,7 +167,7 @@
        (NONE, "Timeout: You can increase the time limit using the \"timeout\" \
               \option (e.g., \"timeout = " ^
               string_of_int (10 + msecs div 1000) ^ "\").")
-     | {outcome = SOME UnknownError, ...} =>
+     | {outcome = SOME (UnknownError _), ...} =>
        (* Failure sometimes mean timeout, unfortunately. *)
        (NONE, "Failure: No proof was found with the current time limit. You \
               \can increase the time limit using the \"timeout\" \

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Dec 17 21:47:13 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Dec 17 22:15:08 2010 +0100
@@ -396,7 +396,7 @@
                          I)
                   |>> (if measure_run_time then split_time else rpair NONE)
                 val (tstplike_proof, outcome) =
-                  extract_tstplike_proof_and_outcome complete res_code
+                  extract_tstplike_proof_and_outcome verbose complete res_code
                       proof_delims known_failures output
               in (output, msecs, tstplike_proof, outcome) end
             val readable_names = debug andalso overlord
@@ -503,11 +503,12 @@
   | failure_from_smt_failure (SMT_Failure.Abnormal_Termination code) =
     (case AList.lookup (op =) smt_failures code of
        SOME failure => failure
-     | NONE => UnknownError)
+     | NONE => UnknownError ("Abnormal termination with exit code " ^
+                             string_of_int code ^ "."))
   | failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
   | failure_from_smt_failure (SMT_Failure.Other_Failure msg) =
     if String.isPrefix internal_error_prefix msg then InternalError
-    else UnknownError
+    else UnknownError msg
 
 (* FUDGE *)
 val smt_max_iters = Unsynchronized.ref 8