raise on encountering '$(' or '$)' within a comment

[benjub]

(as I proposed in https://github.com/metamath/metamath-exe/pull/84#issuecomment-1130652037).

Now raises, like metamath.c, on the three following "comments":

$( $( $)
$( z$( $)
$( $)z $)

[david-a-wheeler]

Metamath.exe really complains about z$( ?

I would have expected that to be fine.

[digama0]

I believe the rationale is to allow for whitespace-insensitive searching for the end of the comment. This justifies rejecting tokens containing an embedded $), and embedded $( is useful to ensure that verifiers that implement (whitespace insensitive) comment nesting agree with those that just use a regex regarding the beginning and end of comments.

[david-a-wheeler]

@digama0 - okay, that makes sense. I'm just surprised. Making the tools do things consistently makes sense to me.

[benjub]

To @david-a-wheeler, @digama0, @jkingdon:

benoit@ordi$ cat test2.mm
$( $( $)
$( z$( $)
$( $)z $)
benoit@ordi$ ./metamath 'read test2.mm' 'quit'
Metamath - Version 0.198 7-Aug-2021           Type HELP for help, EXIT to exit.
MM> read test2.mm
Reading source file "test2.mm"... 29 bytes

?Error on line 1 of file "test2.mm":
$( $( $)
   ^^
Nested comments are not allowed.

?Error on line 2 of file "test2.mm":
$( z$( $)
    ^^
Nested comments are not allowed.

?Error on line 3 of file "test2.mm":
$( $)z $)
     ^
A keyword must be followed by white space.

?Error on line 3 of file "test2.mm":
$( $)z $)
       ^^
A comment terminator was found outside of a comment.

29 bytes were read into the source buffer.
The source has 0 statements; 0 are $a and 0 are $p.
?Error:
$( $)z $)
     ^
There should be no tokens after the last statement.

5 errors were found.
MM> quit

When reading the third line, it seems that metamath.c's problem is not really that there is a '$)' substring within a comment, but that '$)' is not followed by white space, and then there is an extra error complaining about the second '$)'.

[digama0]

I think metamath is correct here: in $( $)z $), the comment is actually $( $), but it has some junk immediately after the comment end marker (not okay), and then a dangling $) (not okay). The ambiguity of which comment close to match to is of course why they are rejected in the first place.