# HG changeset patch
# User boehmes
# Date 1251714135 -7200
# Node ID c714141777926ba29633674c25753961a0a988ac
# Parent  a1a5589207adab75249798772864a529aa7570f1
Mirabelle sledgehammer: added option to keep problem files, enabled "metis" switch again (was accidentally removed)

diff -r a1a5589207ad -r c71414177792 src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Aug 31 09:28:50 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Aug 31 12:22:15 2009 +0200
@@ -18,10 +18,21 @@
     |> Source.exhaust
   end
 
+fun safe init done f x =
+  let
+    val y = init x
+    val z = Exn.capture f y
+    val _ = done y
+  in Exn.release z end
+
+val proverK = "prover"
+val keepK = "keep"
+val metisK = "metis"
+
 fun sledgehammer_action args {pre=st, ...} =
   let
     val prover_name =
-      AList.lookup (op =) args "prover"
+      AList.lookup (op =) args proverK
       |> the_default (hd (space_explode " " (AtpManager.get_atps ())))
 
     val thy = Proof.theory_of st
@@ -30,13 +41,23 @@
     val timeout = AtpManager.get_timeout () 
 
     (* run sledgehammer *)
-    val (success, message, thm_names) =
+    fun init NONE = !AtpWrapper.destdir
+      | init (SOME path) =
+          let
+            (* Warning: we implicitly assume single-threaded execution here! *)
+            val old = !AtpWrapper.destdir
+            val _ = AtpWrapper.destdir := path
+          in old end
+    fun done path = AtpWrapper.destdir := path
+    fun sh _ =
       let
         val (success, (message, thm_names), _, _, _) =
           prover timeout NONE NONE prover_name 1 (Proof.get_goal st)
       in (success, message, SOME thm_names) end
       handle ResHolClause.TOO_TRIVIAL => (true, "trivial", SOME [])
            | ERROR msg => (false, "error: " ^ msg, NONE)
+    val (success, message, thm_names) = safe init done sh
+      (AList.lookup (op =) args keepK)
 
     (* try metis *)
     fun get_thms ctxt = maps (thms_of_name ctxt)
@@ -45,7 +66,8 @@
      (if try (Mirabelle.can_apply (metis thms)) st = SOME true
       then "success"
       else "failure")
-    val msg = apply_metis (get_thms (Proof.context_of st) (these thm_names))
+    val msg = if not (AList.defined (op =) args metisK) then ""
+      else apply_metis (get_thms (Proof.context_of st) (these thm_names))
   in
     if success
     then SOME ("success (" ^ prover_name ^ ": " ^ message ^ ")" ^ msg)