equal
deleted
inserted
replaced
138 Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name || |
138 Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name || |
139 Parse.xname >> Loose; |
139 Parse.xname >> 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 (":", NONE) Keyword.empty_keywords; |
143 val query_keywords = Keyword.add_keywords (":", NONE) Keyword.empty_keywords; |
144 |
144 |
145 in |
145 in |
146 |
146 |
147 fun read_query pos str = |
147 fun read_query pos str = |
148 Outer_Syntax.scan query_keywords pos str |
148 Outer_Syntax.scan query_keywords pos str |