more robust read_query;
authorwenzelm
Thu Aug 08 23:34:52 2013 +0200 (2013-08-08)
changeset 5292571e938856a03
parent 52922 d1bcb4479a2f
child 52926 6415d95bf7a2
more robust read_query;
avoid pointless position, which is always line 1 for single-line input;
src/Pure/Tools/find_theorems.ML
src/Tools/WWW_Find/find_theorems.ML
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Thu Aug 08 20:43:54 2013 +0200
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Thu Aug 08 23:34:52 2013 +0200
     1.3 @@ -21,7 +21,7 @@
     1.4    }
     1.5  
     1.6    val read_criterion: Proof.context -> string criterion -> term criterion
     1.7 -  val parse_query: string -> (bool * string criterion) list
     1.8 +  val read_query: Position.T -> string -> (bool * string criterion) list
     1.9  
    1.10    val xml_of_query: term query -> XML.tree
    1.11    val query_of_xml: XML.tree -> term query
    1.12 @@ -624,22 +624,20 @@
    1.13        Parse.!!! (Scan.option Parse.nat -- Scan.optional (Parse.reserved "with_dups" >> K false) true
    1.14          --| Parse.$$$ ")")) (NONE, true);
    1.15  
    1.16 -val query_parser = Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion));
    1.17 +val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);
    1.18  
    1.19  in
    1.20  
    1.21 -(* FIXME proper wrapper for parser combinator *)
    1.22 -fun parse_query str =
    1.23 -  (str ^ ";")
    1.24 -  |> Outer_Syntax.scan Position.start
    1.25 +fun read_query pos str =
    1.26 +  Outer_Syntax.scan pos str
    1.27    |> filter Token.is_proper
    1.28 -  |> Scan.error query_parser
    1.29 -  |> fst;
    1.30 +  |> Scan.error (Scan.finite Token.stopper (Parse.!!! (query --| Scan.ahead Parse.eof)))
    1.31 +  |> #1;
    1.32  
    1.33  val _ =
    1.34    Outer_Syntax.improper_command @{command_spec "find_theorems"}
    1.35      "find theorems meeting specified criteria"
    1.36 -    (options -- query_parser >> (fn ((opt_lim, rem_dups), spec) =>
    1.37 +    (options -- query >> (fn ((opt_lim, rem_dups), spec) =>
    1.38        Toplevel.keep (fn state =>
    1.39          Pretty.writeln (pretty_theorems_cmd state opt_lim rem_dups spec))));
    1.40  
    1.41 @@ -650,7 +648,7 @@
    1.42  (** PIDE query operation **)
    1.43  
    1.44  val _ =
    1.45 -  Query_Operation.register "find_theorems" (fn state => fn query =>
    1.46 -    Pretty.string_of (pretty_theorems_cmd state NONE false (maps parse_query query)));
    1.47 +  Query_Operation.register "find_theorems" (fn st => fn args =>
    1.48 +    Pretty.string_of (pretty_theorems_cmd st NONE false (maps (read_query Position.none) args)));
    1.49  
    1.50  end;
     2.1 --- a/src/Tools/WWW_Find/find_theorems.ML	Thu Aug 08 20:43:54 2013 +0200
     2.2 +++ b/src/Tools/WWW_Find/find_theorems.ML	Thu Aug 08 23:34:52 2013 +0200
     2.3 @@ -16,7 +16,7 @@
     2.4      val args = Symtab.lookup arg_data;
     2.5  
     2.6      val query_str = the_default "" (args "query");
     2.7 -    fun get_query () = Find_Theorems.parse_query query_str;
     2.8 +    fun get_query () = Find_Theorems.read_query Position.none query_str;
     2.9  
    2.10      val limit = case args "limit" of
    2.11          NONE => default_limit