more frugal keywords;
authorwenzelm
Wed Nov 05 21:10:38 2014 +0100 (2014-11-05)
changeset 5890555160ef37e8f
parent 58904 f49c4f883c58
child 58906 29788e989d61
more frugal keywords;
src/Pure/Tools/find_consts.ML
src/Pure/Tools/find_theorems.ML
     1.1 --- a/src/Pure/Tools/find_consts.ML	Wed Nov 05 20:49:30 2014 +0100
     1.2 +++ b/src/Pure/Tools/find_consts.ML	Wed Nov 05 21:10:38 2014 +0100
     1.3 @@ -140,10 +140,12 @@
     1.4  
     1.5  val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);
     1.6  
     1.7 +val query_keywords = Keyword.add (":", NONE) Keyword.empty_keywords;
     1.8 +
     1.9  in
    1.10  
    1.11  fun read_query pos str =
    1.12 -  Outer_Syntax.scan (Keyword.get_keywords ()) pos str
    1.13 +  Outer_Syntax.scan query_keywords pos str
    1.14    |> filter Token.is_proper
    1.15    |> Scan.error (Scan.finite Token.stopper (Parse.!!! (query --| Scan.ahead Parse.eof)))
    1.16    |> #1;
     2.1 --- a/src/Pure/Tools/find_theorems.ML	Wed Nov 05 20:49:30 2014 +0100
     2.2 +++ b/src/Pure/Tools/find_theorems.ML	Wed Nov 05 21:10:38 2014 +0100
     2.3 @@ -526,10 +526,12 @@
     2.4  
     2.5  val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);
     2.6  
     2.7 +val query_keywords = Keyword.add (":", NONE) Keyword.empty_keywords;
     2.8 +
     2.9  in
    2.10  
    2.11  fun read_query pos str =
    2.12 -  Outer_Syntax.scan (Keyword.get_keywords ()) pos str
    2.13 +  Outer_Syntax.scan query_keywords pos str
    2.14    |> filter Token.is_proper
    2.15    |> Scan.error (Scan.finite Token.stopper (Parse.!!! (query --| Scan.ahead Parse.eof)))
    2.16    |> #1;