Open billh0420 opened 1 year ago
Note: lines 97-107 might be clearer if written as:
if text->Js.String2.charAt(foundIdx - 1)->isWhitespace == false { // need leading whitespace
setIdx(foundIdx+1)
}
else if !(endOfFile.contents || ch.contents->isWhitespace) { // need trailing whitespace or endOfFile
setIdx(foundIdx+1)
}
else {
result.contents = Some(Some(text->Js_string2.substring(~from=beginIdx, ~to_=foundIdx)))
setIdx(foundIdx + 2)
}
This avoids advancing idx by 2 always and then moving idx back by 1 in the two exceptional cases.
I didn't test this new code: not sure if you even want it.
Would you prefer I make the change and test it?
Thanks for submitting this PR. I compared how metamath-exe processes comments vs mm-lamp. Unfortunately, it appeared to be not so easy task. When I put $( something ($) more $)
somewhere in the middle of an *.mm file, metamath-exe failed to parse such a file, similarly mm-lamp fails. Ideally I want mm-lamp to behave the same way as metamath-exe does. Currently they seem to behave similarly in terms of parsing comments. But according to the Metamath book, the end of a comment indeed should be preceded by a whitespace (Appendix E, Metamath Language EBNF). This could be a bug in metamath-exe too. I need more time to analyze this situation.
I believe whitespace must precede the closing comment token.
The current version does the following:
The first three examples should continue looking for closing comment token.
The last example should yield " something ($) more "