ClosingCommentInString.lagda.tex

%% This file was automatically generated by agda2lagda 0.2025.9.5.

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

\begin{code}
 and other garbage @#$% that appears now as Agda code!"
-}
\end{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).

\begin{code}
This should be still commented-out. -}
\end{code}

The reverse situation:

\begin{code}
test = "Never put comment opening {- inside a string!"

postulate
  ThisShouldNotBeCommentedOut : Set

-- -} This should be text, not code!!
\end{code}

SNAFU.