# HG changeset patch
# User blanchet
# Date 1271445485 -7200
# Node ID ba06ef722163fda04dd71b2d4ddc112dfe0ead7b
# Parent  35b9f0db49a0b80fed76ca74f9145198f0073354
by default, don't try to start ATPs that aren't installed

diff -r 35b9f0db49a0 -r ba06ef722163 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Apr 16 20:51:15 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Apr 16 21:18:05 2010 +0200
@@ -96,11 +96,19 @@
   val extend = I
   fun merge p : T = AList.merge (op =) (K true) p)
 
+(* Don't even try to start ATPs that are not installed.
+   Hack: Should not rely on naming convention. *)
+val filter_atps =
+  space_explode " "
+  #> filter (fn s => String.isPrefix "remote_" s orelse
+                     getenv (String.map Char.toUpper s ^ "_HOME") <> "")
+  #> space_implode " "
+
 val set_default_raw_param = Data.map o AList.update (op =) o unalias_raw_param
 fun default_raw_params thy =
   Data.get thy
   |> fold (AList.default (op =))
-          [("atps", [!atps]),
+          [("atps", [filter_atps (!atps)]),
            ("full_types", [if !full_types then "true" else "false"]),
            ("timeout", let val timeout = !timeout in
                          [if timeout <= 0 then "none"