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

feat: guard_msgs to escapes trailing newlines #3617

Merged
merged 1 commit into from
Mar 12, 2024

Conversation

nomeata
Copy link
Contributor

@nomeata nomeata commented Mar 6, 2024

This makes trailing whitespace visible and protectes them against
trimming by the editor, by appending the symbol ⏎ to such a line (and
also to any line that ends with such a symbol, to avoid ambiguities in
the case the message already had that symbol).

(Only the code action output / docstring parsing is affected; the error message as sent
to the InfoView is unaffected.)

Fixes #3571

This makes trailing whitespace visible and protectes them against
trimming by the editor, by appending the symbol ⏎ to such a line (and
also to any line that ends with such a symbol, to avoid ambiguities in
the case the message already had that symbol).

Fixes #3571
@nomeata nomeata requested a review from kmill March 6, 2024 09:18
@nomeata nomeata added the awaiting-review Waiting for someone to review the PR label Mar 6, 2024
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 6, 2024 09:27 Inactive
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Mar 6, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase f0a762ea4d2a78b1f0e484ffa9154c5f495d4c39 --onto ae492265fec103aa834d897bf9f68c94d10f0785. (2024-03-06 09:35:08)

@nomeata
Copy link
Contributor Author

nomeata commented Mar 11, 2024

@kmill, would you be interested in having a look if this approach is reasonable?

@kmill
Copy link
Collaborator

kmill commented Mar 11, 2024

I'm a bit uncertain about using a new symbol () for line breaks, but I've tried to come up with other solutions and there doesn't seem to be anything better.

  1. is unlikely to be used in messages, so we won't see very much of the ⏎⏎ encoding.
  2. is a good graphical representation for the concept.

Maybe @digama0 has thoughts about this? I approve conditional on Mario's approval (or if Mario conditionally approves on my approval).

@nomeata
Copy link
Contributor Author

nomeata commented Mar 11, 2024

Thanks!

Fractional reviewing :-)

@digama0
Copy link
Collaborator

digama0 commented Mar 12, 2024

Yes, I'm fine with this solution. I don't think we will see much of this symbol anyway, because we want to avoid trailing whitespace altogether, but at least this won't cause heisenbugs that trigger only on save.

@nomeata nomeata added this pull request to the merge queue Mar 12, 2024
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Mar 12, 2024
@nomeata nomeata added this pull request to the merge queue Mar 12, 2024
Merged via the queue into master with commit 07dac67 Mar 12, 2024
13 of 19 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
awaiting-review Waiting for someone to review the PR toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Development

Successfully merging this pull request may close these issues.

guard_msgs and trailing space
4 participants