# HG changeset patch
# User krauss
# Date 1306768068 -7200
# Node ID 76e1d25c6357c73718de925c92d989c059424979
# Parent  e0d4841c5b4a3f2e86d27439e7908687d1c33fba
separate query parsing from actual search

diff -r e0d4841c5b4a -r 76e1d25c6357 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Mon May 30 17:00:38 2011 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Mon May 30 17:07:48 2011 +0200
@@ -15,9 +15,17 @@
 
   val tac_limit: int Unsynchronized.ref
   val limit: int Unsynchronized.ref
+
+  val read_criterion: Proof.context -> string criterion -> term criterion
+
   val find_theorems: Proof.context -> thm option -> int option -> bool ->
+    (bool * term criterion) list -> int option * (Facts.ref * thm) list
+  val find_theorems_cmd: Proof.context -> thm option -> int option -> bool ->
     (bool * string criterion) list -> int option * (Facts.ref * thm) list
   val filter_theorems: Proof.context -> theorem list -> thm option ->
+    int option -> bool -> (bool * term criterion) list ->
+    int option * theorem list
+  val filter_theorems_cmd: Proof.context -> theorem list -> thm option ->
     int option -> bool -> (bool * string criterion) list ->
     int option * theorem list
 
@@ -420,7 +428,7 @@
 
 val limit = Unsynchronized.ref 40;
 
-fun filter_theorems ctxt theorems opt_goal opt_limit rem_dups raw_criteria =
+fun filter_theorems ctxt theorems opt_goal opt_limit rem_dups criteria =
   let
     val assms =
       Proof_Context.get_fact ctxt (Facts.named "local.assms")
@@ -428,7 +436,6 @@
     val add_prems = Seq.hd o TRY (Method.insert_tac assms 1);
     val opt_goal' = Option.map add_prems opt_goal;
 
-    val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
     val filters = map (filter_criterion ctxt opt_goal') criteria;
 
     fun find_all theorems =
@@ -451,11 +458,18 @@
 
   in find theorems end;
 
-fun find_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
-  filter_theorems ctxt (map Internal (all_facts_of ctxt)) opt_goal opt_limit
+fun filter_theorems_cmd ctxt theorems opt_goal opt_limit rem_dups raw_criteria =
+  filter_theorems ctxt theorems opt_goal opt_limit rem_dups
+    (map (apsnd (read_criterion ctxt)) raw_criteria);
+
+fun gen_find_theorems filter ctxt opt_goal opt_limit rem_dups raw_criteria =
+  filter ctxt (map Internal (all_facts_of ctxt)) opt_goal opt_limit
      rem_dups raw_criteria
   |> apsnd (map (fn Internal f => f));
 
+val find_theorems = gen_find_theorems filter_theorems;
+val find_theorems_cmd = gen_find_theorems filter_theorems_cmd;
+
 fun pretty_theorem ctxt (Internal (thmref, thm)) = Pretty.block
       [Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1,
         Display.pretty_thm ctxt thm]
@@ -471,7 +485,7 @@
 
     val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
     val (foundo, theorems) = filter_theorems ctxt (map Internal (all_facts_of ctxt))
-      opt_goal opt_limit rem_dups raw_criteria;
+      opt_goal opt_limit rem_dups criteria;
     val returned = length theorems;
 
     val tally_msg =
diff -r e0d4841c5b4a -r 76e1d25c6357 src/Tools/WWW_Find/find_theorems.ML
--- a/src/Tools/WWW_Find/find_theorems.ML	Mon May 30 17:00:38 2011 +0200
+++ b/src/Tools/WWW_Find/find_theorems.ML	Mon May 30 17:07:48 2011 +0200
@@ -210,7 +210,7 @@
         val ctxt = Proof_Context.init_global (Thy_Info.get_theory thy_name);
         val query = get_query ();
         val (othmslen, thms) = apsnd rev
-          (Find_Theorems.find_theorems ctxt NONE (SOME limit) with_dups query);
+          (Find_Theorems.find_theorems_cmd ctxt NONE (SOME limit) with_dups query);
         val thmslen = length thms;
         fun thm_row args = Xhtml.write send (html_thm ctxt args);
       in