proper outer syntax category, e.g. relevant for PIDE markup;
authorwenzelm
Mon Jul 06 15:34:45 2015 +0200 (2015-07-06)
changeset 60664263a8f15faf3
parent 60663 143ac4d9504a
child 60665 61be352b1f79
proper outer syntax category, e.g. relevant for PIDE markup;
src/Pure/Tools/find_consts.ML
     1.1 --- a/src/Pure/Tools/find_consts.ML	Mon Jul 06 14:27:03 2015 +0200
     1.2 +++ b/src/Pure/Tools/find_consts.ML	Mon Jul 06 15:34:45 2015 +0200
     1.3 @@ -134,9 +134,9 @@
     1.4  local
     1.5  
     1.6  val criterion =
     1.7 -  Parse.reserved "strict" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Strict ||
     1.8    Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name ||
     1.9 -  Parse.xname >> Loose;
    1.10 +  Parse.reserved "strict" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.typ) >> Strict ||
    1.11 +  Parse.typ >> Loose;
    1.12  
    1.13  val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);
    1.14