# HG changeset patch
# User blanchet
# Date 1341956163 -7200
# Node ID 712d49104b13c2547c919c3d33a83ec65da398fa
# Parent  8fa803f5a7319a2de707f339ba5d7ea320faa4da
don't ask E to generate a detailed proofs if not needed

diff -r 8fa803f5a731 -r 712d49104b13 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Jul 10 23:36:03 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Jul 10 23:36:03 2012 +0200
@@ -213,7 +213,8 @@
 
 (* E *)
 
-fun is_new_e_version () = (string_ord (getenv "E_VERSION", "1.2") = GREATER)
+fun is_recent_e_version () = (string_ord (getenv "E_VERSION", "1.3") <> LESS)
+fun is_new_e_version () = (string_ord (getenv "E_VERSION", "1.6") <> LESS)
 
 val tstp_proof_delims =
   [("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation"),
@@ -289,23 +290,35 @@
        else "")
     end
 
+fun e_shell_level_argument full_proof =
+  if is_new_e_version () then
+    " --pcl-shell-level=" ^ (if full_proof then "0" else "2")
+  else
+    ""
+
 fun effective_e_selection_heuristic ctxt =
-  if is_new_e_version () then Config.get ctxt e_selection_heuristic else e_autoN
+  if is_recent_e_version () then Config.get ctxt e_selection_heuristic
+  else e_autoN
 
-fun e_kbo () = if is_new_e_version () then "KBO6" else "KBO"
+fun e_kbo () = if is_recent_e_version () then "KBO6" else "KBO"
 
 val e_config : atp_config =
   {exec = (["E_HOME"], "eproof"),
    required_vars = [],
    arguments =
-     fn ctxt => fn _ => fn heuristic => fn timeout =>
+     fn ctxt => fn full_proof => fn heuristic => fn timeout =>
         fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) =>
         "--tstp-in --tstp-out --output-level=5 --silent " ^
         e_selection_weight_arguments ctxt heuristic sel_weights ^ " " ^
         e_term_order_info_arguments gen_weights gen_prec ord_info ^ " " ^
         "--term-ordering=" ^ (if is_lpo then "LPO4" else e_kbo ()) ^ " " ^
-        "--cpu-limit=" ^ string_of_int (to_secs 2 timeout),
-   proof_delims = tstp_proof_delims,
+        "--cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^
+        e_shell_level_argument full_proof,
+   proof_delims =
+     (* work-around for bug in "epclextract" version 1.6 *)
+     ("# SZS status Theorem\n# SZS output start Saturation.",
+      "# SZS output end Saturation.") ::
+     tstp_proof_delims,
    known_failures =
      [(TimedOut, "Failure: Resource limit exceeded (time)"),
       (TimedOut, "time limit exceeded")] @