Hi Jean,

>>>>> jfbu <jfbu@free.fr> writes:

> But isn't there a bug even for the use case one wants the verbatim to
> be inserted inside the comment?

> (which wasn't my case)

> Look at commented out last line, and at the added blank line.

> \documentclass{article}

> \begin{document}
> % \begin{verbatim}
> % This is a comment
> \def\foo#1{foo}
> % another comment

> % \end{verbatim}
> % \end{document}

Thanks for your comments.  I agree that the current behavior is not
totally satisfactory, and expect the attatched patch would crudely
resolve this particular issue.  However, the relevant codes must be
involved in a lot, lot of different cases, so it might not be valid for
some other cases.  I'm not sure currently.

Regards,
Ikumi Keita