# HG changeset patch
# User blanchet
# Date 1271923982 -7200
# Node ID 0e24322474a4b171635cd42bbc30dbcfd404b64c
# Parent  25e69e93954d1964ec4110fc4a43b0635a9803c1
postprocess ATP output in "overlord" mode to make it more readable

diff -r 25e69e93954d -r 0e24322474a4 src/HOL/Tools/ATP_Manager/atp_wrapper.ML
--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Wed Apr 21 17:06:26 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Thu Apr 22 10:13:02 2010 +0200
@@ -112,12 +112,17 @@
 
     (* write out problem file and call prover *)
     fun cmd_line probfile =
-      if Config.get ctxt measure_runtime then
-        "TIMEFORMAT='%3U'; { time " ^ space_implode " " [File.shell_path cmd,
-        args, File.shell_path probfile] ^ " ; } 2>&1"
-      else
-        space_implode " " ["exec", File.shell_path cmd, args,
-        File.shell_path probfile, "2>&1"];
+      (if Config.get ctxt measure_runtime then
+         "TIMEFORMAT='%3U'; { time " ^ space_implode " " [File.shell_path cmd,
+         args, File.shell_path probfile] ^ " ; } 2>&1"
+       else
+         space_implode " " ["exec", File.shell_path cmd, args,
+         File.shell_path probfile, "2>&1"]) ^
+      (if overlord then
+         " | sed 's/,/, /g' | sed 's/\\([=|]\\)/ \\1 /g' | sed 's/! =/ !=/g' \
+         \| sed 's/  / /g'"
+       else
+         "")
     fun split_time s =
       let
         val split = String.tokens (fn c => str c = "\n");
@@ -160,7 +165,7 @@
       if success then
         proof_text ctxt minimize_command proof internal_thm_names th subgoal
       else if failure <> "" then
-        (failure, [])
+        (failure ^ "\n", [])
       else
         ("Unknown ATP error: " ^ proof ^ ".\n", [])
   in