proper outer syntax category, e.g. relevant for PIDE markup;
--- a/src/Pure/Tools/find_consts.ML Mon Jul 06 14:27:03 2015 +0200
+++ b/src/Pure/Tools/find_consts.ML Mon Jul 06 15:34:45 2015 +0200
@@ -134,9 +134,9 @@
local
val criterion =
- Parse.reserved "strict" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Strict ||
Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name ||
- Parse.xname >> Loose;
+ Parse.reserved "strict" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.typ) >> Strict ||
+ Parse.typ >> Loose;
val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);