d3bb097 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fixed doc comments in multi-line comments bug

commitd3bb097924684230804e331f72c0868988802da5 authorAhmad Salim Al-Sibahi <asal@itu.dk> dateSun 22 Sep 2013, 14:24 (13 years ago) parent914a765

1 file changed+2

unifiedsplit

src/Idris/Parser.hs+2

@@ -112,6 +112,8 @@ multiLineComment = try (string "{-" *> (string "-}") *> pure ())

112112 where inCommentChars :: MonadicParsing m => m ()

113113 inCommentChars = try (string "-}" *> pure ())

114114 <|> try (multiLineComment *> inCommentChars)

115+ <|> try (docComment '|' *> inCommentChars)

116+ <|> try (docComment '^' *> inCommentChars)

115117 <|> try (skipSome (noneOf startEnd) *> inCommentChars)

116118 <|> oneOf startEnd *> inCommentChars

117119 <?> "end of comment"