# HG changeset patch
# User wenzelm
# Date 1376772348 -7200
# Node ID e18a028b345ca766dfdf9bba23eb0291528a5b31
# Parent  3d22b952118bce11907842c51817ac23d6f49e33
prefer system option sledgehammer_timeout, with standard GUI in jEdit Plugin Options;

diff -r 3d22b952118b -r e18a028b345c src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- 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"]),
diff -r 3d22b952118b -r e18a028b345c src/HOL/Tools/etc/options
--- 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)"
+
diff -r 3d22b952118b -r e18a028b345c src/Tools/jEdit/src/sledgehammer_dockable.scala
--- 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)
 }