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

fix parsing error : return commands even when the end of the file contains parsing error #1086

Merged
merged 8 commits into from
May 7, 2024

Conversation

Alidra
Copy link
Member

@Alidra Alidra commented Apr 18, 2024

When working with Vscode or Emacs, if a Lambdapi file contains parsing errors, the parsing phase should return the commands that have been successfully parsed (this is already the case with the command line Lambdapi).

This PR fixes this issue.

Additionally, this PR changes the way navigating the proofs is done in Vscode with the navigate until cursor.
Instead of stopping the green zone at the beginning of current the line, the green zone is expended to the end of the current command.

Finally, this PR fixes stops the green zone before the { delimiter (and incidentally begin delimiter) to avoid that the LSP server answers with subgoals of the next tactic missing the current one as described in issue #1049

@Alidra Alidra linked an issue Apr 18, 2024 that may be closed by this pull request
@fblanqui fblanqui marked this pull request as ready for review April 18, 2024 17:09
@Alidra Alidra requested a review from fblanqui April 19, 2024 08:32
…gin of the line to display logs related to missing tokens at the end of the file
@Alidra Alidra self-assigned this Apr 26, 2024
@Alidra Alidra linked an issue Apr 26, 2024 that may be closed by this pull request
@Alidra
Copy link
Member Author

Alidra commented Apr 26, 2024

@fblanqui , Can you check if the behavior described in this PR suites you?

@Alidra
Copy link
Member Author

Alidra commented May 7, 2024

@fblanqui, as discussed earlier today, the modifications in this PR work fine with both Vscode and Emacs.
We still need to fix the syntax error message in Emacs terminal but it is better to do it in a separate PR.

Thus, I believe the PR can be merged.

@fblanqui fblanqui merged commit a884b81 into Deducteam:master May 7, 2024
20 checks passed
@fblanqui
Copy link
Member

fblanqui commented May 7, 2024

Thanks Abdelghani!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Parsing failure prevents from showing log messages in debug terminal Displaying subgoals on VS Code
2 participants