[ fix #3057 ] properly handle char literals in comments

This commit is contained in:
Guillaume Allais 2023-08-28 13:25:35 +01:00 committed by G. Allais
parent a4ccb27c83
commit e3214586a5
5 changed files with 11 additions and 1 deletions

View File

@ -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

View File

@ -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",

View File

@ -0,0 +1,4 @@
{-
c : Char
c = '"'
-}

View File

@ -0,0 +1 @@
1/1: Building Test (Test.idr)

3
tests/idris2/literals001/run Executable file
View File

@ -0,0 +1,3 @@
rm -rf build
$1 --no-color --console-width 0 --no-banner -c Test.idr