31156f0 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

support trailing quotes in verbatim string literals

Since verbatim strings in Idris don't support escapes, it seems appropriate to have them consume all '"' characters before the closing "\"\"\"". This is the approach taken by Scala. This means the following verbatim strings now parse, and produce the parenthesized values, which are expressed as standard strings. * `"""""""` (`"\""`) * `""""hello""""` (`"\"hello\""`) * `"""""a"""""""` (`"\"\"a\"\"\"\""`) * `"""trailing """"` (`"trailing \""`)

commit31156f0341ec9cdcdb8cbb6c4aae1db6a7be79a1 authorMichael Morgan <morgan.michael@me.com> dateThu 16 Nov 2017, 15:14 (9 years ago) parent21ab196

1 file changed+3−2

compare with master

unifiedsplit

src/Idris/Parser/Expr.hs+3−2

src/Idris/Parser/Expr.hs+3−2

@@ -1461,7 +1461,7 @@ constant = P.choice [ do fc <- reservedFC name; return (ty, fc)

14611461

14621462@

14631463VerbatimString_t ::=

1464− '\"\"\"' ~'\"\"\"' '\"\"\"'

1464+ '\"\"\"' ~'\"\"\"' '\"'* '\"\"\"'

14651465;

14661466@

14671467 -}

@@ -1469,8 +1469,9 @@ verbatimStringLiteral :: IdrisParser (String, FC)

14691469verbatimStringLiteral = token $ do (FC f start _) <- getFC

14701470 P.try $ string "\"\"\""

14711471 str <- P.manyTill P.anyChar $ P.try (string "\"\"\"")

1472+ moreQuotes <- P.many $ P.char '"'

14721473 (FC _ _ end) <- getFC

1473− return (str, FC f start end)

1474+ return (str ++ moreQuotes, FC f start end)

14741475

14751476{- | Parses a static modifier

14761477