src/Pure/Tools/find_theorems.ML
changeset 52925 71e938856a03
parent 52865 02a7e7180ee5
child 52926 6415d95bf7a2
     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;