In Emacs, when a proof is started but the end token is missing at the end of the proof, the console doesn't show the log message Unexpected token: "".
PR #1086 has fixed the issue of showing log messages (for instance when using the verbose command) even when parsing errors occur . However, in Emacs the parsing error message is still missing
For instance, in Vscode navigating the proofs to the end of the folowing file
verbose 3;
constant symbol T : TYPE;
opaque symbol trivial : T → T → T → T
≔ begin
produces the following logs :
verbose 3
somefile.lp:2:0-25
symbol T : TYPE
[somefile.lp:5:7] Unexpected token: "".
But in Emacs, it produces the following logs (last line is missing)
In Emacs, when a proof is started but the
endtoken is missing at the end of the proof, the console doesn't show the log messageUnexpected token: "".PR #1086 has fixed the issue of showing log messages (for instance when using the verbose command) even when parsing errors occur . However, in Emacs the parsing error message is still missing
For instance, in Vscode navigating the proofs to the end of the folowing file
produces the following logs :
But in Emacs, it produces the following logs (last line is missing)