# HG changeset patch
# User wenzelm
# Date 1375997692 -7200
# Node ID 71e938856a03edc7ab0390824347940ecf083775
# Parent  d1bcb4479a2f8fe4679453cf29b86428bd8efea4
more robust read_query;
avoid pointless position, which is always line 1 for single-line input;

diff -r d1bcb4479a2f -r 71e938856a03 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Thu Aug 08 20:43:54 2013 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Thu Aug 08 23:34:52 2013 +0200
@@ -21,7 +21,7 @@
   }
 
   val read_criterion: Proof.context -> string criterion -> term criterion
-  val parse_query: string -> (bool * string criterion) list
+  val read_query: Position.T -> string -> (bool * string criterion) list
 
   val xml_of_query: term query -> XML.tree
   val query_of_xml: XML.tree -> term query
@@ -624,22 +624,20 @@
       Parse.!!! (Scan.option Parse.nat -- Scan.optional (Parse.reserved "with_dups" >> K false) true
         --| Parse.$$$ ")")) (NONE, true);
 
-val query_parser = Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion));
+val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);
 
 in
 
-(* FIXME proper wrapper for parser combinator *)
-fun parse_query str =
-  (str ^ ";")
-  |> Outer_Syntax.scan Position.start
+fun read_query pos str =
+  Outer_Syntax.scan pos str
   |> filter Token.is_proper
-  |> Scan.error query_parser
-  |> fst;
+  |> Scan.error (Scan.finite Token.stopper (Parse.!!! (query --| Scan.ahead Parse.eof)))
+  |> #1;
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "find_theorems"}
     "find theorems meeting specified criteria"
-    (options -- query_parser >> (fn ((opt_lim, rem_dups), spec) =>
+    (options -- query >> (fn ((opt_lim, rem_dups), spec) =>
       Toplevel.keep (fn state =>
         Pretty.writeln (pretty_theorems_cmd state opt_lim rem_dups spec))));
 
@@ -650,7 +648,7 @@
 (** PIDE query operation **)
 
 val _ =
-  Query_Operation.register "find_theorems" (fn state => fn query =>
-    Pretty.string_of (pretty_theorems_cmd state NONE false (maps parse_query query)));
+  Query_Operation.register "find_theorems" (fn st => fn args =>
+    Pretty.string_of (pretty_theorems_cmd st NONE false (maps (read_query Position.none) args)));
 
 end;
diff -r d1bcb4479a2f -r 71e938856a03 src/Tools/WWW_Find/find_theorems.ML
--- a/src/Tools/WWW_Find/find_theorems.ML	Thu Aug 08 20:43:54 2013 +0200
+++ b/src/Tools/WWW_Find/find_theorems.ML	Thu Aug 08 23:34:52 2013 +0200
@@ -16,7 +16,7 @@
     val args = Symtab.lookup arg_data;
 
     val query_str = the_default "" (args "query");
-    fun get_query () = Find_Theorems.parse_query query_str;
+    fun get_query () = Find_Theorems.read_query Position.none query_str;
 
     val limit = case args "limit" of
         NONE => default_limit