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

Change Language Config to Fix Indents #1015

Merged
merged 1 commit into from
Jan 29, 2025

Conversation

Durbatuluk1701
Copy link
Contributor

Couple Changes Here:

  • Change the language configuration files to .language-configuration.json (as suggested by lang guide)
  • Modify the language configuration to address Incorrect Indentation with Show Proof. #247 (manual proof indentation with negative lookbehind)
  • Modify the wordPattern definition to correctly identify identifiers in Rocq (items with a ' within them before would not be correctly suggested by intellisense)
  • Added some auto-indent features for Sections, Module Types, and Modules.

IndentFixesGif

Of Note:

  • Changes were made to make it so that match statements do not auto-indent (related to Bad Indentation with match ... end #248), but I am not sure the solution is optimal? I am seeking feedback if we think the behavior exhibited below is better or worse than the current approach?
    MatchIndentChanges

@Durbatuluk1701
Copy link
Contributor Author

I still believe #158 would be helpful (and could work on addressing it in the future), but I think hopefully these changes would make some of the default indentation that occurs while typing better

@rtetley
Copy link
Collaborator

rtetley commented Jan 29, 2025

I believe this is already an improvement so I'll merge ! Thanks !

@rtetley rtetley merged commit c7a0bd3 into coq:main Jan 29, 2025
28 checks passed
@Durbatuluk1701 Durbatuluk1701 deleted the indentation_fixes branch January 29, 2025 15:20
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.

2 participants