# HG changeset patch
# User krauss
# Date 1306768068 -7200
# Node ID ac769b5edd1d29d068fa992c7911e0e4987c143e
# Parent  76e1d25c6357c73718de925c92d989c059424979
exported raw query parser; removed inconsistent clone

diff -r 76e1d25c6357 -r ac769b5edd1d src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Mon May 30 17:07:48 2011 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Mon May 30 17:07:48 2011 +0200
@@ -17,6 +17,7 @@
   val limit: int Unsynchronized.ref
 
   val read_criterion: Proof.context -> string criterion -> term criterion
+  val query_parser: (bool * string criterion) list parser
 
   val find_theorems: Proof.context -> thm option -> int option -> bool ->
     (bool * term criterion) list -> int option * (Facts.ref * thm) list
@@ -530,10 +531,12 @@
         --| Parse.$$$ ")")) (NONE, true);
 in
 
+val query_parser = Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion));
+
 val _ =
   Outer_Syntax.improper_command "find_theorems" "print theorems meeting specified criteria"
     Keyword.diag
-    (options -- Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion))
+    (options -- query_parser
       >> (fn ((opt_lim, rem_dups), spec) =>
         Toplevel.no_timing o
         Toplevel.keep (fn state =>
diff -r 76e1d25c6357 -r ac769b5edd1d src/Tools/WWW_Find/find_theorems.ML
--- a/src/Tools/WWW_Find/find_theorems.ML	Mon May 30 17:07:48 2011 +0200
+++ b/src/Tools/WWW_Find/find_theorems.ML	Mon May 30 17:07:48 2011 +0200
@@ -159,18 +159,6 @@
 
 end;
 
-val criterion =
-  Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Find_Theorems.Name ||
-  Parse.reserved "intro" >> K Find_Theorems.Intro ||
-  Parse.reserved "elim" >> K Find_Theorems.Elim ||
-  Parse.reserved "dest" >> K Find_Theorems.Dest ||
-  Parse.reserved "solves" >> K Find_Theorems.Solves ||
-  Parse.reserved "simp" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.term) >> Find_Theorems.Simp ||
-  Parse.term >> Find_Theorems.Pattern;
-
-val parse_query =
-  Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion));
-
 fun app_index f xs = fold_index (fn x => K (f x)) xs ();
 
 fun find_theorems (req as ScgiReq.Req {request_method, query_string, ...},
@@ -193,7 +181,7 @@
       |> (fn s => s ^ ";")
       |> Outer_Syntax.scan Position.start
       |> filter Token.is_proper
-      |> Scan.error parse_query
+      |> Scan.error Find_Theorems.query_parser
       |> fst;
 
     val limit =