1.1 --- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Aug 31 09:28:50 2009 +0200
     1.2 +++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Aug 31 12:22:15 2009 +0200
     1.3 @@ -18,10 +18,21 @@
     1.4      |> Source.exhaust
     1.5    end
     1.6  
     1.7 +fun safe init done f x =
     1.8 +  let
     1.9 +    val y = init x
    1.10 +    val z = Exn.capture f y
    1.11 +    val _ = done y
    1.12 +  in Exn.release z end
    1.13 +
    1.14 +val proverK = "prover"
    1.15 +val keepK = "keep"
    1.16 +val metisK = "metis"
    1.17 +
    1.18  fun sledgehammer_action args {pre=st, ...} =
    1.19    let
    1.20      val prover_name =
    1.21 -      AList.lookup (op =) args "prover"
    1.22 +      AList.lookup (op =) args proverK
    1.23        |> the_default (hd (space_explode " " (AtpManager.get_atps ())))
    1.24  
    1.25      val thy = Proof.theory_of st
    1.26 @@ -30,13 +41,23 @@
    1.27      val timeout = AtpManager.get_timeout () 
    1.28  
    1.29      (* run sledgehammer *)
    1.30 -    val (success, message, thm_names) =
    1.31 +    fun init NONE = !AtpWrapper.destdir
    1.32 +      | init (SOME path) =
    1.33 +          let
    1.34 +            (* Warning: we implicitly assume single-threaded execution here! *)
    1.35 +            val old = !AtpWrapper.destdir
    1.36 +            val _ = AtpWrapper.destdir := path
    1.37 +          in old end
    1.38 +    fun done path = AtpWrapper.destdir := path
    1.39 +    fun sh _ =
    1.40        let
    1.41          val (success, (message, thm_names), _, _, _) =
    1.42            prover timeout NONE NONE prover_name 1 (Proof.get_goal st)
    1.43        in (success, message, SOME thm_names) end
    1.44        handle ResHolClause.TOO_TRIVIAL => (true, "trivial", SOME [])
    1.45             | ERROR msg => (false, "error: " ^ msg, NONE)
    1.46 +    val (success, message, thm_names) = safe init done sh
    1.47 +      (AList.lookup (op =) args keepK)
    1.48  
    1.49      (* try metis *)
    1.50      fun get_thms ctxt = maps (thms_of_name ctxt)
    1.51 @@ -45,7 +66,8 @@
    1.52       (if try (Mirabelle.can_apply (metis thms)) st = SOME true
    1.53        then "success"
    1.54        else "failure")
    1.55 -    val msg = apply_metis (get_thms (Proof.context_of st) (these thm_names))
    1.56 +    val msg = if not (AList.defined (op =) args metisK) then ""
    1.57 +      else apply_metis (get_thms (Proof.context_of st) (these thm_names))
    1.58    in
    1.59      if success
    1.60      then SOME ("success (" ^ prover_name ^ ": " ^ message ^ ")" ^ msg)