94 type T = raw_param list |
94 type T = raw_param list |
95 val empty = default_default_params |> map (apsnd single) |
95 val empty = default_default_params |> map (apsnd single) |
96 val extend = I |
96 val extend = I |
97 fun merge p : T = AList.merge (op =) (K true) p) |
97 fun merge p : T = AList.merge (op =) (K true) p) |
98 |
98 |
|
99 (* Don't even try to start ATPs that are not installed. |
|
100 Hack: Should not rely on naming convention. *) |
|
101 val filter_atps = |
|
102 space_explode " " |
|
103 #> filter (fn s => String.isPrefix "remote_" s orelse |
|
104 getenv (String.map Char.toUpper s ^ "_HOME") <> "") |
|
105 #> space_implode " " |
|
106 |
99 val set_default_raw_param = Data.map o AList.update (op =) o unalias_raw_param |
107 val set_default_raw_param = Data.map o AList.update (op =) o unalias_raw_param |
100 fun default_raw_params thy = |
108 fun default_raw_params thy = |
101 Data.get thy |
109 Data.get thy |
102 |> fold (AList.default (op =)) |
110 |> fold (AList.default (op =)) |
103 [("atps", [!atps]), |
111 [("atps", [filter_atps (!atps)]), |
104 ("full_types", [if !full_types then "true" else "false"]), |
112 ("full_types", [if !full_types then "true" else "false"]), |
105 ("timeout", let val timeout = !timeout in |
113 ("timeout", let val timeout = !timeout in |
106 [if timeout <= 0 then "none" |
114 [if timeout <= 0 then "none" |
107 else string_of_int timeout ^ " s"] |
115 else string_of_int timeout ^ " s"] |
108 end)] |
116 end)] |