Handle comments inside &&&
-bulleted blocks better
#82
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
The interaction of comments and bulleted blocks previously caused surprising number of newlines to show up. This PR fixes this.
In particular, the following code is now considered correctly-formatted
Previously, there would be unnecessary newlines added after every comment. This would happen because comments have a forced-hardline after them, while
&&&
(and|||
) bullets have a forced hardline before them, causing the number of hardlines to double-up, leading to surprising looking code.Example sub-optimal code with the old surprising behavior (issue reported by Johanna (@JoPolzin)):
Note: this particular change causes a single-line change to the Verus vstd snapshot, but still requires a tiny amount of coordination to prevent spurious CI failures there before releasing (should not block merging, just blocks release, and should likely bump the minor version, rather than just patch version).