Merge pull request #253 from gallais/nested-comments

[ fix ] properly nesting multiline comments

src/Parser/Lexer.idr

@@ -46,10 +46,12 @@ comment = is '-' <+> is '-' <+> many (isNot '\n')
 toEndComment : (k : Nat) -> Recognise (k /= 0)
 toEndComment Z = empty
 toEndComment (S k)
-             = some (pred (\c => c /= '-' && c /= '{'))
+             = some (pred (\c => c /= '-' && c /= '{' && c /= '"'))
                       <+> toEndComment (S k)
            <|> is '{' <+> is '-' <+> toEndComment (S (S k))
            <|> is '-' <+> is '}' <+> toEndComment k
+           <|> comment <+> toEndComment (S k)
+           <|> stringLit <+> toEndComment (S k)
            <|> is '{' <+> toEndComment (S k)
            <|> is '-' <+> toEndComment (S k)
 

tests/Main.idr

@@ -31,7 +31,7 @@ idrisTests
        "basic021", "basic022", "basic023", "basic024", "basic025",
        "basic026", "basic027", "basic028", "basic029", "basic030",
        "basic031", "basic032", "basic033", "basic034", "basic035",
-       "basic036",
+       "basic036", "basic037",
        -- Coverage checking
        "coverage001", "coverage002", "coverage003", "coverage004",
        "coverage005", "coverage006",

tests/idris2/basic037/Comments.idr

@@ -0,0 +1,23 @@
+-- This is a valid comment {-
+-- It should not lead to a parse error if nested in a
+-- multiline comment
+
+{- Hence this test
+
+-- This is a valid comment {-
+-- It should not lead to a parse error if nested in a
+-- multiline comment
+
+-}
+
+myString : String
+myString = "Similarly, this is a valid string literal {- "
+-- So we should be able to put it in a multiline comment
+
+{- Hence this test
+
+myString : String
+myString = "Similarly, this is a valid string literal {- "
+-- So we should be able to put it in a multiline comment
+
+-}

tests/idris2/basic037/expected

@@ -0,0 +1,2 @@
+1/1: Building Comments (Comments.idr)
+Main> Bye for now!

tests/idris2/basic037/run

@@ -0,0 +1,3 @@
+echo ':q' | $1 --no-banner --no-prelude Comments.idr
+
+rm -rf build