diff --git a/src/Parser/Interface.md b/src/Parser/Interface.md index 3dc4251..fd0f433 100644 --- a/src/Parser/Interface.md +++ b/src/Parser/Interface.md @@ -198,6 +198,7 @@ Lift a parser producing a `List` or `List1` of `Char` into a parser producing a `String` ```idris +-- TODO: Rename these export parseString : Parser (List Char) -> Parser String parseString x = do @@ -250,6 +251,40 @@ exactString str with (asList str) pure input ``` +Wrap a parser in delimiter characters, discarding the value of the delimiters + +```idris +export +delimited : (before, after : Char) -> Parser a -> Parser a +delimited before after x = do + starting_state <- save + _ <- parseExactChar before + val <- x + Just _ <- tryMaybe $ parseExactChar after + | _ => throw $ + MkParseError starting_state "Unmatched delimiter \{show before}" + pure val +``` + +Consume any number of characters of the provided character class and discard the +result. Also a version for doing so on both sides of a provided parser + +```idris +export +nom : Parser Char -> Parser () +nom x = do + _ <- many x + pure () + +export +surround : (around : Parser Char) -> (item : Parser a) -> Parser a +surround around item = do + nom around + val <- item + nom around + pure val +``` + ### Composition of boolean functions ```idris