agda2lagda-0.2020.11.1: test/ClosingCommentInString.agda

-- This demonstrates a known issue:
-- The parser is not aware of strings, thus,
-- a closing block comment delimiter inside a string
-- is taken as a closing block comment delimiter.

-- Without nested comments:

{- This is commented-out.
test = "A weird string with comment closing -} and other garbage @#$% that appears now as Agda code!"
-}

-- With nested comments:

{-
{- This is commented-out.
test = "A weird string with comment closing -} and other garbage @#$%!"
-- NB: this confuses even Agda (at the time of writing, version 2.6.1).
-}
This should be still commented-out. -}

-- The reverse situation:

test = "Never put comment opening {- inside a string!"

postulate
  ThisShouldNotBeCommentedOut : Set

-- -} This should be text, not code!!

-- SNAFU.