ClosingCommentInString.lagda.md

<!-- This file was automatically generated by agda2lagda 0.2023.3.25. -->

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
 -->
```agda
 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).
 -->
```agda
This should be still commented-out. -}
```

The reverse situation:

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

postulate
  ThisShouldNotBeCommentedOut : Set

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

SNAFU.