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.

Sign up for GitHub

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

Jump to bottom

Minor Fixes in the Emacs extension #1168

Merged
merged 4 commits into from
Jan 2, 2025
Merged

Minor Fixes in the Emacs extension #1168

merged 4 commits into from
Jan 2, 2025

Conversation

Alidra
Copy link
Member

@Alidra Alidra commented Dec 27, 2024 •
edited
Loading

This PR fixes some minor issues in the Emacs extension (package). Specifically :

  • The Goals panel is recentred to show the first goal in case of many assumptions and avoid having to scroll down.
  • When proofs are navigated, if the last command is reached, the navigation continues to the end of file to display the last error messages if any (in particular the issue described in In Emacs, the syntax error message at the end of a file, is not displayed in the console #1111 where the end; token is missing)
  • Check that the Goals and Logs buffers are displayed before displaying logs and goals when proofs are navigated

This was linked to issues Dec 27, 2024
In Emacs, the syntax error message at the end of a file, is not displayed in the console #1111
Closed
emacs: automatically scroll down the Goals buffer #1153
Closed
@Alidra Alidra requested a review from fblanqui December 27, 2024 19:07
@Alidra
Copy link
Member Author

Alidra commented Dec 27, 2024

Please note that in case no next command exists but some empty lines, theses empty lines are highlighted to the end of file. I dont know if this is ok?

@fblanqui
Copy link
Member

Hi Abdelghani. Thank you for your PR. It seems to solve #1111 but not #1153. Take for instance the file rules.lp at line 76 in
lpProof_sur_cantor.zip using the master branch of lambdapi-stdlib.

@Alidra
Copy link
Member Author

Alidra commented Dec 31, 2024

Hi Frédéric,
I believe it is fixed now. You can check if you wish.

@fblanqui
Copy link
Member

fblanqui commented Jan 2, 2025

Hi. This still doesn't work for me. See the screen capture below:
Capture d’écran_2025-01-02_10-46-30

@fblanqui
Copy link
Member

fblanqui commented Jan 2, 2025

Sorry it works well now; I forgot to pull.

@fblanqui
Copy link
Member

fblanqui commented Jan 2, 2025

Capture d’écran_2025-01-02_10-58-12

@fblanqui fblanqui merged commit 15d4eea into Deducteam:master Jan 2, 2025
22 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@fblanqui fblanqui Awaiting requested review from fblanqui

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
2 participants
@Alidra @fblanqui