Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

In Emacs, the syntax error message at the end of a file, is not displayed in the console #1111

Open
Alidra opened this issue May 7, 2024 · 0 comments
Assignees
Labels

Comments

@Alidra
Copy link
Member

Alidra commented 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 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
@Alidra 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
@fblanqui fblanqui added the emacs label Nov 22, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

2 participants