exported raw query parser; removed inconsistent clone
authorkrauss
Mon May 30 17:07:48 2011 +0200 (2011-05-30)
changeset 43068ac769b5edd1d
parent 43067 76e1d25c6357
child 43069 88e45168272c
exported raw query parser; removed inconsistent clone
src/Pure/Tools/find_theorems.ML
src/Tools/WWW_Find/find_theorems.ML
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Mon May 30 17:07:48 2011 +0200
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Mon May 30 17:07:48 2011 +0200
     1.3 @@ -17,6 +17,7 @@
     1.4    val limit: int Unsynchronized.ref
     1.5  
     1.6    val read_criterion: Proof.context -> string criterion -> term criterion
     1.7 +  val query_parser: (bool * string criterion) list parser
     1.8  
     1.9    val find_theorems: Proof.context -> thm option -> int option -> bool ->
    1.10      (bool * term criterion) list -> int option * (Facts.ref * thm) list
    1.11 @@ -530,10 +531,12 @@
    1.12          --| Parse.$$$ ")")) (NONE, true);
    1.13  in
    1.14  
    1.15 +val query_parser = Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion));
    1.16 +
    1.17  val _ =
    1.18    Outer_Syntax.improper_command "find_theorems" "print theorems meeting specified criteria"
    1.19      Keyword.diag
    1.20 -    (options -- Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion))
    1.21 +    (options -- query_parser
    1.22        >> (fn ((opt_lim, rem_dups), spec) =>
    1.23          Toplevel.no_timing o
    1.24          Toplevel.keep (fn state =>
     2.1 --- a/src/Tools/WWW_Find/find_theorems.ML	Mon May 30 17:07:48 2011 +0200
     2.2 +++ b/src/Tools/WWW_Find/find_theorems.ML	Mon May 30 17:07:48 2011 +0200
     2.3 @@ -159,18 +159,6 @@
     2.4  
     2.5  end;
     2.6  
     2.7 -val criterion =
     2.8 -  Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Find_Theorems.Name ||
     2.9 -  Parse.reserved "intro" >> K Find_Theorems.Intro ||
    2.10 -  Parse.reserved "elim" >> K Find_Theorems.Elim ||
    2.11 -  Parse.reserved "dest" >> K Find_Theorems.Dest ||
    2.12 -  Parse.reserved "solves" >> K Find_Theorems.Solves ||
    2.13 -  Parse.reserved "simp" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.term) >> Find_Theorems.Simp ||
    2.14 -  Parse.term >> Find_Theorems.Pattern;
    2.15 -
    2.16 -val parse_query =
    2.17 -  Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion));
    2.18 -
    2.19  fun app_index f xs = fold_index (fn x => K (f x)) xs ();
    2.20  
    2.21  fun find_theorems (req as ScgiReq.Req {request_method, query_string, ...},
    2.22 @@ -193,7 +181,7 @@
    2.23        |> (fn s => s ^ ";")
    2.24        |> Outer_Syntax.scan Position.start
    2.25        |> filter Token.is_proper
    2.26 -      |> Scan.error parse_query
    2.27 +      |> Scan.error Find_Theorems.query_parser
    2.28        |> fst;
    2.29  
    2.30      val limit =