1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Mar 20 00:44:30 2012 +0100
1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Mar 20 00:44:30 2012 +0100
1.3 @@ -8,7 +8,6 @@
1.4 sig
1.5 type params = Sledgehammer_Provers.params
1.6
1.7 - val sledgehammerN : string
1.8 val auto : bool Unsynchronized.ref
1.9 val provers : string Unsynchronized.ref
1.10 val timeout : int Unsynchronized.ref
1.11 @@ -29,9 +28,6 @@
1.12 open Sledgehammer_Minimize
1.13 open Sledgehammer_Run
1.14
1.15 -val sledgehammerN = "sledgehammer"
1.16 -val sledgehammer_paramsN = "sledgehammer_params"
1.17 -
1.18 val runN = "run"
1.19 val minN = "min"
1.20 val messagesN = "messages"
1.21 @@ -101,7 +97,8 @@
1.22 ("preplay_timeout", "3")]
1.23
1.24 val alias_params =
1.25 - [("prover", "provers")]
1.26 + [("prover", ("provers", [])),
1.27 + ("dont_preplay", ("preplay_timeout", ["0"]))]
1.28 val negated_alias_params =
1.29 [("no_debug", "debug"),
1.30 ("quiet", "verbose"),
1.31 @@ -133,7 +130,13 @@
1.32
1.33 fun unalias_raw_param (name, value) =
1.34 case AList.lookup (op =) alias_params name of
1.35 - SOME name' => (name', value)
1.36 + SOME (name', []) => (name', value)
1.37 + | SOME (param' as (name', _)) =>
1.38 + if value <> ["false"] then
1.39 + param'
1.40 + else
1.41 + error ("Parameter " ^ quote name ^ " cannot be set to \"false\" \
1.42 + \(cf. " ^ quote name' ^ ").")
1.43 | NONE =>
1.44 case AList.lookup (op =) negated_alias_params name of
1.45 SOME name' => (name', case value of
1.46 @@ -340,7 +343,7 @@
1.47 |> (if prover_name = default_minimize_prover then I else cons prover_name)
1.48 |> space_implode ", "
1.49 in
1.50 - sledgehammerN ^ " " ^ minN ^
1.51 + "sledgehammer" ^ " " ^ minN ^
1.52 (if params = "" then "" else enclose " [" "]" params) ^
1.53 " (" ^ space_implode " " fact_names ^ ")" ^
1.54 (if i = 1 then "" else " " ^ string_of_int i)
1.55 @@ -434,6 +437,6 @@
1.56 (minimize_command [] i) state
1.57 end
1.58
1.59 -val setup = Try.register_tool (sledgehammerN, (40, auto, try_sledgehammer))
1.60 +val setup = Try.register_tool ("sledgehammer", (40, auto, try_sledgehammer))
1.61
1.62 end;