From e3214586a5c7eed97ae07c6f3a525dba98741df3 Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Mon, 28 Aug 2023 13:25:35 +0100
Subject: [PATCH] [ fix #3057 ] properly handle char literals in comments

---
 src/Parser/Lexer/Source.idr       | 3 ++-
 tests/Main.idr                    | 1 +
 tests/idris2/literals001/Test.idr | 4 ++++
 tests/idris2/literals001/expected | 1 +
 tests/idris2/literals001/run      | 3 +++
 5 files changed, 11 insertions(+), 1 deletion(-)
 create mode 100644 tests/idris2/literals001/Test.idr
 create mode 100644 tests/idris2/literals001/expected
 create mode 100755 tests/idris2/literals001/run

diff --git a/src/Parser/Lexer/Source.idr b/src/Parser/Lexer/Source.idr
index a963fb5b3..bc4c3d60c 100644
--- a/src/Parser/Lexer/Source.idr
+++ b/src/Parser/Lexer/Source.idr
@@ -150,10 +150,11 @@ mutual
   toEndComment : (k : Nat) -> Recognise (k /= 0)
   toEndComment Z = empty
   toEndComment (S k)
-               = some (pred (\c => c /= '-' && c /= '{' && c /= '"'))
+               = some (pred (\c => c /= '-' && c /= '{' && c /= '"' && c /= '\''))
                         <+> (eof <|> toEndComment (S k))
              <|> is '{' <+> singleBrace k
              <|> is '-' <+> singleDash k
+             <|> (charLit <|> pred (== '\'')) <+> toEndComment (S k)
              <|> stringLit <+> toEndComment (S k)
 
   ||| After reading a single brace, we may either finish reading an
diff --git a/tests/Main.idr b/tests/Main.idr
index 993658fc9..078ca1a0e 100644
--- a/tests/Main.idr
+++ b/tests/Main.idr
@@ -44,6 +44,7 @@ idrisTestsBasic = MkTestPool "Fundamental language features" [] Nothing
        "basic061", "basic062", "basic063", "basic064", "basic065",
        "basic066", "basic067", "basic068", "basic069", "basic070",
        "idiom001",
+       "literals001",
        "dotted001",
        "rewrite001",
        "interpolation001", "interpolation002", "interpolation003",
diff --git a/tests/idris2/literals001/Test.idr b/tests/idris2/literals001/Test.idr
new file mode 100644
index 000000000..fe1c8e2b9
--- /dev/null
+++ b/tests/idris2/literals001/Test.idr
@@ -0,0 +1,4 @@
+{-
+c : Char
+c = '"'
+-}
diff --git a/tests/idris2/literals001/expected b/tests/idris2/literals001/expected
new file mode 100644
index 000000000..31e5db7f3
--- /dev/null
+++ b/tests/idris2/literals001/expected
@@ -0,0 +1 @@
+1/1: Building Test (Test.idr)
diff --git a/tests/idris2/literals001/run b/tests/idris2/literals001/run
new file mode 100755
index 000000000..71e882e50
--- /dev/null
+++ b/tests/idris2/literals001/run
@@ -0,0 +1,3 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --no-banner -c Test.idr