equal
deleted
inserted
replaced
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 |