prefer system option sledgehammer_timeout, with standard GUI in jEdit Plugin Options;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sat Aug 17 22:27:41 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sat Aug 17 22:45:48 2013 +0200
@@ -9,7 +9,6 @@
type params = Sledgehammer_Provers.params
val provers : string Unsynchronized.ref
- val timeout : int Unsynchronized.ref
val default_params : Proof.context -> (string * string) list -> params
end;
@@ -61,7 +60,6 @@
(*** parameters ***)
val provers = Unsynchronized.ref ""
-val timeout = Unsynchronized.ref 30
val _ =
ProofGeneral.preference_string ProofGeneral.category_proof
@@ -71,9 +69,9 @@
"Default automatic provers (separated by whitespace)"
val _ =
- ProofGeneral.preference_int ProofGeneral.category_proof
+ ProofGeneral.preference_option ProofGeneral.category_proof
NONE
- timeout
+ @{option sledgehammer_timeout}
"Sledgehammer: Time Limit"
"ATPs will be interrupted after this time (in seconds)"
@@ -240,7 +238,7 @@
[("provers", [case !provers of
"" => default_provers_param_value ctxt
| s => s]),
- ("timeout", let val timeout = !timeout in
+ ("timeout", let val timeout = Options.default_int @{option sledgehammer_timeout} in
[if timeout <= 0 then "none"
else string_of_int timeout]
end)]
@@ -500,13 +498,12 @@
(case try Toplevel.proof_of st of
SOME state =>
let
- val [provers_arg, timeout_arg, isar_proofs_arg] = args;
+ val [provers_arg, isar_proofs_arg] = args;
val ctxt = Proof.context_of state
val override_params =
((if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)]) @
- [("timeout", [timeout_arg]),
- ("isar_proofs", [isar_proofs_arg]),
+ [("isar_proofs", [isar_proofs_arg]),
("blocking", ["true"]),
("minimize", ["true"]),
("debug", ["false"]),
--- a/src/HOL/Tools/etc/options Sat Aug 17 22:27:41 2013 +0200
+++ b/src/HOL/Tools/etc/options Sat Aug 17 22:45:48 2013 +0200
@@ -23,3 +23,9 @@
public option auto_solve_direct : bool = true
-- "run solve_direct automatically"
+
+section "Miscellaneous Tools"
+
+public option sledgehammer_timeout : int = 30
+ -- "ATPs will be interrupted after this time (in seconds)"
+
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Sat Aug 17 22:27:41 2013 +0200
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Sat Aug 17 22:45:48 2013 +0200
@@ -134,7 +134,7 @@
/* controls */
private def clicked {
- sledgehammer.apply_query(List(provers.getText, timeout.text, isar_proofs.selected.toString))
+ sledgehammer.apply_query(List(provers.getText, isar_proofs.selected.toString))
}
private val provers_label = new Label("Provers:") {
@@ -151,12 +151,6 @@
setColumns(30)
}
- private val timeout = new TextField("30.0", 5) {
- tooltip = "Soft time limit for each automatic prover (seconds > 0)"
- verifier = (s: String) =>
- s match { case Properties.Value.Double(x) => x >= 0.0 case _ => false }
- }
-
private val isar_proofs = new CheckBox("Isar proofs") {
tooltip = "Specify whether Isar proofs should be output in addition to metis line"
selected = false
@@ -183,7 +177,7 @@
private val controls =
new FlowPanel(FlowPanel.Alignment.Right)(
- provers_label, Component.wrap(provers), timeout, isar_proofs,
+ provers_label, Component.wrap(provers), isar_proofs,
process_indicator.component, apply_query, cancel_query, locate_query, zoom)
add(controls.peer, BorderLayout.NORTH)
}