equal
deleted
inserted
replaced
522 Parse.!!! (Scan.option Parse.nat -- Scan.optional (Parse.reserved "with_dups" >> K false) true |
522 Parse.!!! (Scan.option Parse.nat -- Scan.optional (Parse.reserved "with_dups" >> K false) true |
523 --| Parse.$$$ ")")) (NONE, true); |
523 --| Parse.$$$ ")")) (NONE, true); |
524 |
524 |
525 val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion); |
525 val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion); |
526 |
526 |
527 val query_keywords = Keyword.add_keywords [(":", NONE)] Keyword.empty_keywords; |
527 val query_keywords = Keyword.add_keywords [((":", @{here}), NONE)] Keyword.empty_keywords; |
528 |
528 |
529 in |
529 in |
530 |
530 |
531 fun read_query pos str = |
531 fun read_query pos str = |
532 Token.explode query_keywords pos str |
532 Token.explode query_keywords pos str |