# HG changeset patch
# User wenzelm
# Date 1374178700 -7200
# Node ID c503730efae539090ee2d669c32eaf622d3adb61
# Parent  51dfdcd88e84cd051aafac5de28859565aa6cef8
proper system options for 'find_theorems';

diff -r 51dfdcd88e84 -r c503730efae5 etc/options
--- a/etc/options	Thu Jul 18 22:00:35 2013 +0200
+++ b/etc/options	Thu Jul 18 22:18:20 2013 +0200
@@ -125,3 +125,13 @@
 
 public option editor_chart_delay : real = 3.0
   -- "delay for chart repainting"
+
+
+section "Miscellaneous Tools"
+
+public option find_theorems_limit : int = 40
+  -- "limit of displayed results"
+
+public option find_theorems_tac_limit : int = 5
+  -- "limit of tactic search for 'solves' criterion"
+
diff -r 51dfdcd88e84 -r c503730efae5 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Thu Jul 18 22:00:35 2013 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Thu Jul 18 22:18:20 2013 +0200
@@ -20,9 +20,6 @@
     criteria: (bool * 'term criterion) list
   }
 
-  val tac_limit: int Unsynchronized.ref
-  val limit: int Unsynchronized.ref
-
   val read_criterion: Proof.context -> string criterion -> term criterion
   val query_parser: (bool * string criterion) list parser
 
@@ -314,11 +311,10 @@
     end
   else NONE;
 
-val tac_limit = Unsynchronized.ref 5;
-
 fun filter_solves ctxt goal =
   let
-    fun etacn thm i = Seq.take (! tac_limit) o etac thm i;
+    fun etacn thm i =
+      Seq.take (Options.default_int @{option find_theorems_tac_limit}) o etac thm i;
     fun try_thm thm =
       if Thm.no_prems thm then rtac thm 1 goal
       else (etacn thm THEN_ALL_NEW (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt)) 1 goal;
@@ -507,8 +503,6 @@
       visible_facts (Proof_Context.facts_of ctxt))
   end;
 
-val limit = Unsynchronized.ref 40;
-
 fun filter_theorems ctxt theorems query =
   let
     val {goal = opt_goal, limit = opt_limit, rem_dups, criteria} = query;
@@ -524,7 +518,7 @@
           else raw_matches;
 
         val len = length matches;
-        val lim = the_default (! limit) opt_limit;
+        val lim = the_default (Options.default_int @{option find_theorems_limit}) opt_limit;
       in (SOME len, drop (Int.max (len - lim, 0)) matches) end;
 
     val find =