PG goes bananas (accepts any string after `{|`)

[samuelgruetter]

The following file is accepted by PG:

Goal False.
Proof.
  {| Hello this is cool.
  {| Is this a new kind of comment? .
  {| Multi-line
     works
     as well!.
Abort.

{| Also works outside a Proof .

But results in a syntax error when compiled with coqc.

It seems that whenever a command starts with {|, PG accepts any string following it, until the dot, but doesn't cause coqtop to do anything.

[Matafou]

Hi. Thanks for reporting. Indeed there is a problem with error detection since a few weeks. I will try to fix that shortly. FTR this does not seem to be fixed by #615.

[Matafou]

No it has actually nothing to do with error detection. It is yet another case where PG splitting the coq file into single commands wrongly. Here the { at start is not detected as a subproof starter, because the token {| is recognized as something else. So the string " {| Hello this is cool." is sent to coq as if it were a single command. But coq take the first {` as one command, and the remainin of the string as another (buggy) one. Two prompts are displayed at once, PG does not support this.

I will try to find time to fix this, but this has low priority since there will always be such corner cases where a buggy file is not correctly split by PG (until PG relies on coq splitting one day).

[Matafou]

Duplicate of #357.