From 08a2f263bba4372a80c217476852f4084fa8b186 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Sun, 26 Jan 2025 20:51:24 -0500 Subject: [PATCH] json: parse char result --- src/Parser/JSON.md | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/Parser/JSON.md b/src/Parser/JSON.md index 87af1dc..b990e54 100644 --- a/src/Parser/JSON.md +++ b/src/Parser/JSON.md @@ -110,7 +110,7 @@ whitespace : Parser Char whitespace = do pnote "Whitespace character" result <- - parseChar (\x => any (== x) $ the (List _) [' ', '\n', '\r', '\t']) id + parseChar (\x => any (== x) $ the (List _) [' ', '\n', '\r', '\t']) case result of GotChar char => pure char GotError err => throwParseError "Expected whitespace, got: \{show err}" @@ -221,9 +221,12 @@ string = do -- TODO: Handle control characters properly stringCharacter : Parser Char stringCharacter = do - e1 <- parseError "Expected non-quote, got quote" - e2 <- parseError "End of input" - parseCharE (not . (== '"')) (\_ => e1) e2 + result <- parseChar (not . (== '"')) + case result of + GotChar char => pure char + GotError err => + throwParseError "Expected string character, got \{show err}" + EndOfInput => throwParseError "Unexpected end of input" ``` ```idris