# HG changeset patch
# User blanchet
# Date 1271937058 -7200
# Node ID fa6d03d42aab3c96a329b376d7397dc105a725c3
# Parent  d868b34d604cb3573826d0fffc064312b42298e1
"remote_e" and "remote_vampire" support TSTP proof output + fix "overlord" mode ATP output postprocessing

diff -r d868b34d604c -r fa6d03d42aab src/HOL/Tools/ATP_Manager/atp_wrapper.ML
--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Thu Apr 22 10:54:56 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Thu Apr 22 13:50:58 2010 +0200
@@ -119,8 +119,12 @@
          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'"
+         " | sed 's/,/, /g' \
+         \| sed 's/\\([^!=]\\)\\([=|]\\)\\([^=]\\)/\\1 \\2 \\3/g' \
+         \| sed 's/! =/ !=/g' \
+         \| sed 's/  / /g' | sed 's/| |/||/g' \
+         \| sed 's/ = = =/===/g' \
+         \| sed 's/= = /== /g'"
        else
          "")
     fun split_time s =
@@ -335,7 +339,8 @@
     "Error: The remote ATP proof is ill-formed.")]
 
 fun remote_prover_config prover_prefix args
-        ({known_failures, max_new_clauses, prefers_theory_relevant, ...}
+        ({known_failures, max_new_clauses, prefers_theory_relevant,
+          supports_isar_proofs, ...}
          : prover_config) : prover_config =
   {command = Path.explode "$ISABELLE_ATP_MANAGER/SystemOnTPTP",
    arguments = (fn timeout =>
@@ -344,7 +349,7 @@
    known_failures = remote_known_failures @ known_failures,
    max_new_clauses = max_new_clauses,
    prefers_theory_relevant = prefers_theory_relevant,
-   supports_isar_proofs = false}
+   supports_isar_proofs = supports_isar_proofs}
 
 val remote_vampire =
   tptp_prover "remote_vampire"