`.}` not detected by PG as syntax error

[clarksmr]

Environment: Mac, Emacs 27.2, Coq 8.13.2, PG 20220310.2253; also VS Code 1.65.2, VSCoq 0.3.6; Coq_Platform_2021.09.0; and the online Scratchpad jsCoq 0.15.0, Coq 8.15.0.

Steps to reproduce:

1. Put this code (copied from #83) in a buffer:

Goal True.
  {apply I.}
Qed.

2. Compile that code with PG.

Expected behavior: The <dot><rbrace> tokens should result in an error: Error: Syntax Error: Lexer: Undefined token.

Actual behavior: The code is compiled without error.

Explanation: VSCode, CoqPlatform, the online Scratchpad, and coqc all exhibit the expected behavior and reject the code. Only PG accepts the code without error.

Examples:

Terminal transcript with coqc:

$ cat dot_rbrace.v
Goal True.
  {apply I.}
Qed.
$ coqc dot_rbrace.v
File "./dot_rbrace.v", line 2, characters 10-12:
Error: Syntax Error: Lexer: Undefined token

Screenshot with PG:

Related: #83 seemed to have the same root cause, but I'm opening a new issue because this isn't about Software Foundations, and that issue is a bit hard to find by searching for the error.

[Matafou]

Indeed pg is far from perfect at splitting a file into commands. This case is known #357. Along with at least those: #612, #592, #58. We definitely need to make things better int his particular case because it probably happens very often.