Skip to content

Conversation

@jim-portegies
Copy link
Contributor

@jim-portegies jim-portegies commented Oct 29, 2025

Description

Refactor of the grammar.

Changes

  • Add compatibility with
  • Refactor the grammar to be more maintainable
  • Allow for removing spaces in grammar, such as the one in "Obtain ", which made that "Obtain\n" would not be colored correctly.
  • More coloring of Vernac
  • Color bullets and braces and differently
  • Add coloring of 'magic'
  • Add unit tests for grammar
  • Fix Obtain such a(n) ...

Testing this PR

Go through the unit tests, see that they are run and that they have enough coverage of different parsing situations.
Moreover, use this PR in waterproof-vscode (in conjunction with impermeable/waterproof-vscode#259), open several exercise sheets and see if they get colored correctly. Play around a bit with spaces and enters to see coloring behaves well with them.

@jim-portegies
Copy link
Contributor Author

Maybe I'm a bit confused about the role of the new tactics.json

@DikieDick
Copy link
Contributor

DikieDick commented Oct 30, 2025

Maybe I'm a bit confused about the role of the new tactics.json

It's not a new tactics.json, but a copied version from waterproof-vscode (I hope up to date) that allows me to test whether all the waterproof tactics parse as a WaterproofTactic. The language package should not really be part of the editor, but instead be integrated into waterproof-vscode. That would eliminate this redudant tactics file and allow users of waterproof-editor to supply their own highlighters/parsers. An example situation where we would want this functionality is if someone is implementing a Lean version of waterproof-vscode with our editor and they want Lean syntax coloring.

Maybe we should discuss this in more detail in person?

@DikieDick
Copy link
Contributor

I still need to add more unit tests to this as well.

Copy link
Contributor

@pimotte pimotte left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Just a cursory review with one comment

Previously the default themeStyle was 'light' and the editor would
initialize the codemirror highlighting as if the theme was 'light'.
This would lead to a period where the theme was incorrectly set if the
user was in a dark style theme. Now we initialize the editor with the
correct theme style, without waiting for a message from the host.
@DikieDick
Copy link
Contributor

@pimotte As I worked on this PR as well, maybe you should be the one to review it :)

Copy link
Contributor

@pimotte pimotte left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good overall. Two remarks:

  • This breaks the dark theme for me. (Works on waterproof-vscode main, breaks on waterproof-vscode main with this PR built and linked) In particular, the lemma statements are practically invisible to me. Fixed when testing with impermeable/waterproof-vscode#259
image
  • You've written unit tests, but sonar doesn't notice coverage on new code. Is the new code uncovered and is the coverage on old code? (Also, the coverage config I think is still broken in general, but I'll pick that up.) Discussed with @DikieDick, fix is in #30

We probably want to figure out the first point before merging, the second is more an FYI.

Copy link
Contributor

@pimotte pimotte left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Critical issues have been addressed. I'm good with merging after considering this comment: #38 (comment)

@sonarqubecloud
Copy link

sonarqubecloud bot commented Nov 3, 2025

Quality Gate Failed Quality Gate failed

Failed conditions
0.0% Coverage on New Code (required ≥ 80%)

See analysis details on SonarQube Cloud

@DikieDick DikieDick merged commit 457a369 into main Nov 3, 2025
4 of 5 checks passed
@DikieDick DikieDick deleted the fix/grammar branch December 28, 2025 17:28
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.

4 participants