# HG changeset patch
# User immler@in.tum.de
# Date 1237041945 -3600
# Node ID db8b10fd51a4f07103853443daae4ee95d40a895
# Parent  0ac3db5a59a8ad820435ffe570a995ed8b0e8ad3
show certain errors to the user

diff -r 0ac3db5a59a8 -r db8b10fd51a4 contrib/SystemOnTPTP/remote
--- a/contrib/SystemOnTPTP/remote	Sat Mar 14 15:15:44 2009 +0100
+++ b/contrib/SystemOnTPTP/remote	Sat Mar 14 15:45:45 2009 +0100
@@ -83,17 +83,13 @@
 
 #catch errors / failure
 if(! $Response->is_success){
-  	print "HTTP-Error: " . $Response->message . "\n";
-    exit(-1);
+  print "HTTP-Error: " . $Response->message . "\n";
+  exit(-1);
 } elsif (exists($Options{'w'})) {
   print $Response->content;
   exit (0);
 } elsif ($Response->content =~ /NO SOLUTION OUTPUT BY SYSTEM/){
-  if ($Response->content =~ /%\s*Result\s*:(.*)\n%\s*Output\s*:(.*)\n%/) {
-    print "No Solution Output\nResult: $1\nOutput: $2\n";
-  } else {
-    print "No Solution Output\n";
-  }
+  print "No Solution Output by System\n";
   exit(-1);
 } elsif ($Response->content =~ /ERROR: Could not form TPTP format derivation/) {
   print "Could not form TPTP format derivation\n";
diff -r 0ac3db5a59a8 -r db8b10fd51a4 src/HOL/Tools/atp_wrapper.ML
--- a/src/HOL/Tools/atp_wrapper.ML	Sat Mar 14 15:15:44 2009 +0100
+++ b/src/HOL/Tools/atp_wrapper.ML	Sat Mar 14 15:45:45 2009 +0100
@@ -78,8 +78,10 @@
     val failure = find_failure proof
     val success = rc = 0 andalso is_none failure
     val message =
-      if success then "Try this command: " ^ produce_answer (proof, thm_names, ctxt, goal, subgoalno)
-      else "Could not prove goal."
+      if isSome failure then "Proof attempt failed."
+      else if rc <> 0 then "Proof attempt failed: " ^ proof 
+      else "Try this command: " ^ produce_answer (proof, thm_names, ctxt, goal, subgoalno)
+
     val _ = if isSome failure
       then Output.debug (fn () => "Sledgehammer failure: " ^ the failure ^ "\nOutput: " ^ proof)
       else ()