You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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)
verbose 3
somefile.lp:2:0-25
symbol T : TYPE
The text was updated successfully, but these errors were encountered:
Alidra
changed the title
In Emacs if a Goal
In Emacs, the syntax error message at the end of a file, is not displayed in the console
May 7, 2024
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 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)
The text was updated successfully, but these errors were encountered: