src/Pure/Tools/find_consts.ML
changeset 60664 263a8f15faf3
parent 60610 f52b4b0c10c4
child 60667 d86c449d30ba
equal deleted inserted replaced
60663:143ac4d9504a 60664:263a8f15faf3
   132 (* command syntax *)
   132 (* command syntax *)
   133 
   133 
   134 local
   134 local
   135 
   135 
   136 val criterion =
   136 val criterion =
   137   Parse.reserved "strict" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Strict ||
       
   138   Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name ||
   137   Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name ||
   139   Parse.xname >> Loose;
   138   Parse.reserved "strict" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.typ) >> Strict ||
       
   139   Parse.typ >> Loose;
   140 
   140 
   141 val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);
   141 val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);
   142 
   142 
   143 val query_keywords = Keyword.add_keywords [((":", @{here}), NONE)] Keyword.empty_keywords;
   143 val query_keywords = Keyword.add_keywords [((":", @{here}), NONE)] Keyword.empty_keywords;
   144 
   144