Gutter highlighting broken #4287
Labels
release-blocker
Must be resolved before the next release
Comments
|
After git bisecting, this regression appeared on merging #4201 |
|
I reproduced the issue in a test and I am going to work on it |
This was referenced Jul 14, 2023
MikaelMayer
added a commit
that referenced
this issue
Jul 19, 2023
robin-aws
added a commit
that referenced
this issue
Jul 20, 2023
Fixes #4287 Co-authored-by: Robin Salkeld <[email protected]>
keyboardDrummer
added a commit
that referenced
this issue
Aug 4, 2023
This PR fixes #4287 The computation of the number of lines was done improperly for empty files and wasn't migrated properly for non-empty files, which resulted in gutter icons to never expand as before. I modified the tests so that it's now possible to fully simulate a variable number of line and more general insertions, which helped me first reproduce the issue and then ensure that the fix was correct. Also, I renamed "Next" to "Replace" in the tests so that it better reflects what the edit is supposed to do: replace the entire line. I added the variant "Insert" and described https://github.com/dafny-lang/dafny/pull/4288/files#diff-81426824e7dbbe14c1b83ee3acd4998ddd7b565b09c355e835c7e101b930f4c5R184 what the variants mean I made it possible also for the tests to perform several changes at once, so that I can simulate not just removing a comment like "//Insert:", but also replacing \n by newlines and \\ by single backslashes. <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small> --------- Co-authored-by: Remy Willems <[email protected]>
keyboardDrummer
added a commit
to keyboardDrummer/dafny
that referenced
this issue
Sep 15, 2023
This PR fixes dafny-lang#4287 The computation of the number of lines was done improperly for empty files and wasn't migrated properly for non-empty files, which resulted in gutter icons to never expand as before. I modified the tests so that it's now possible to fully simulate a variable number of line and more general insertions, which helped me first reproduce the issue and then ensure that the fix was correct. Also, I renamed "Next" to "Replace" in the tests so that it better reflects what the edit is supposed to do: replace the entire line. I added the variant "Insert" and described https://github.com/dafny-lang/dafny/pull/4288/files#diff-81426824e7dbbe14c1b83ee3acd4998ddd7b565b09c355e835c7e101b930f4c5R184 what the variants mean I made it possible also for the tests to perform several changes at once, so that I can simulate not just removing a comment like "//Insert:", but also replacing \n by newlines and \\ by single backslashes. <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small> --------- Co-authored-by: Remy Willems <[email protected]>
keyboardDrummer
added a commit
that referenced
this issue
Sep 19, 2023
This PR fixes #4287 The computation of the number of lines was done improperly for empty files and wasn't migrated properly for non-empty files, which resulted in gutter icons to never expand as before. I modified the tests so that it's now possible to fully simulate a variable number of line and more general insertions, which helped me first reproduce the issue and then ensure that the fix was correct. Also, I renamed "Next" to "Replace" in the tests so that it better reflects what the edit is supposed to do: replace the entire line. I added the variant "Insert" and described https://github.com/dafny-lang/dafny/pull/4288/files#diff-81426824e7dbbe14c1b83ee3acd4998ddd7b565b09c355e835c7e101b930f4c5R184 what the variants mean I made it possible also for the tests to perform several changes at once, so that I can simulate not just removing a comment like "//Insert:", but also replacing \n by newlines and \\ by single backslashes. <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small> --------- Co-authored-by: Remy Willems <[email protected]>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
This bug wasn't there in 4.1.0 but is in the latest nightly.
Create a new Dafny file.
Write manually (don't copy paste)
You'll get this::
The text was updated successfully, but these errors were encountered: