@@ -119,6 +119,20 @@ choice : (xs : List Lexer) -> {auto ok : NonEmpty xs} -> Lexer
119choice (x :: []) = x
119choice (x :: []) = x
120choice (x :: xs@(_ :: _)) = x <|> choice xs
120choice (x :: xs@(_ :: _)) = x <|> choice xs
122+||| Repeat the sub-lexer `l` zero or more times until the lexer
123+||| `stopBefore` is encountered. `stopBefore` will not be consumed.
124+||| Not guaranteed to consume input.
126+manyUntil : (stopBefore : Recognise c) -> (l : Lexer) -> Recognise False
127+manyUntil stopBefore l = many (reject stopBefore <+> l)
129+||| Repeat the sub-lexer `l` zero or more times until the lexer
130+||| `stopAfter` is encountered, and consume it. Guaranteed to
131+||| consume if `stopAfter` consumes.
133+manyThen : (stopAfter : Recognise c) -> (l : Lexer) -> Recognise c
134+manyThen stopAfter l = manyUntil stopAfter l <+> stopAfter
122||| Recognise many instances of `l` until an instance of `end` is
136||| Recognise many instances of `l` until an instance of `end` is
123||| encountered.
137||| encountered.
@@ -291,7 +305,7 @@ symbols = some symbol
291||| delimiting lexers
305||| delimiting lexers
293surround : (start : Lexer) -> (end : Lexer) -> (l : Lexer) -> Lexer
307surround : (start : Lexer) -> (end : Lexer) -> (l : Lexer) -> Lexer
294−surround start end l = start <+> many (reject end <+> l) <+> end
308+surround start end l = start <+> manyThen end l
296||| Recognise zero or more occurrences of a sub-lexer surrounded
310||| Recognise zero or more occurrences of a sub-lexer surrounded
297||| by the same quote lexer on both sides (useful for strings)
311||| by the same quote lexer on both sides (useful for strings)