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: Code action support #2021

Merged
merged 59 commits into from
Aug 26, 2022
Merged
Changes from 1 commit
Commits
Show all changes
59 commits
Select commit Hold shift + click to select a range
071a50f
Initial support for code actions on the LSP
MikaelMayer Apr 13, 2022
ca200df
Support for plugin system, default dummy quick fix to wrap errors wit…
MikaelMayer Apr 13, 2022
b6b0e95
Insert the failing error at the beginning of the block
MikaelMayer Apr 13, 2022
741174f
Insert failing postcondition at the end.
MikaelMayer Apr 14, 2022
2f51467
Refactored to add comments
MikaelMayer Apr 14, 2022
caf2971
More refactoring
MikaelMayer Apr 14, 2022
5495a40
First code action test working
MikaelMayer Apr 14, 2022
e14f3ed
Added code actions tests
MikaelMayer Apr 14, 2022
62b05c1
Added two tests to verify indentation is kept in the presence of tabs
MikaelMayer Apr 14, 2022
0526479
Verify that code actions work inside an if else statement
MikaelMayer Apr 14, 2022
8530409
Fixed warnings
MikaelMayer Apr 14, 2022
f6578d7
Make it work with anonymous files as well
MikaelMayer Apr 15, 2022
4fb9ac6
Merge branch 'master' into feat-code-actions
MikaelMayer May 2, 2022
dff29f3
Refactored verification quick fix into its own QuickFix class
MikaelMayer May 2, 2022
6e8b10b
WIP on quick fixer
MikaelMayer May 10, 2022
2213f74
Lazy computation of code actions
MikaelMayer May 11, 2022
0a4bbd7
Fixed the tests
MikaelMayer May 11, 2022
5c32824
Two more tests to ensure we have a default increasing indentation.
MikaelMayer May 11, 2022
6c24c17
Better support for simple cases
MikaelMayer May 11, 2022
1526720
Deep support for code action plugins + tests
MikaelMayer May 11, 2022
9c8da89
Fixed a crash that happens from time to time.
MikaelMayer May 11, 2022
459e67d
Merge branch 'master' into feat-code-actions
MikaelMayer May 11, 2022
d781d01
Fixed a test
MikaelMayer May 18, 2022
410e571
Merge branch 'feat-code-actions' of https://github.com/dafny-lang/daf…
MikaelMayer May 18, 2022
d263cbf
Merge branch 'master' into feat-code-actions
MikaelMayer May 18, 2022
1c6cb46
Fixed merge
MikaelMayer May 18, 2022
5240d50
Merge branch 'master' into feat-code-actions
MikaelMayer May 18, 2022
2aaea69
Separate QuickFixer from the other Dafny plugins
MikaelMayer May 25, 2022
815337f
Refactored classes
MikaelMayer May 25, 2022
4a4a99b
Updated doc
MikaelMayer May 25, 2022
b4306d7
More refactoring
MikaelMayer May 25, 2022
e015b0a
More refactoring
MikaelMayer May 25, 2022
b45e006
More refactorings
MikaelMayer May 25, 2022
e6aa3d2
Get latest document for code actions
MikaelMayer May 25, 2022
9e270af
More English fix
MikaelMayer May 26, 2022
e11951f
Merge branch 'master' into feat-code-actions
MikaelMayer May 27, 2022
0c57999
Review comments + tutorial
MikaelMayer May 27, 2022
6ba73f3
More review comments
MikaelMayer May 27, 2022
05c3a2f
Merge branch 'master' into feat-code-actions
MikaelMayer Jun 7, 2022
d9f32ce
Merge branch 'master' into feat-code-actions
MikaelMayer Jun 27, 2022
82bc0ec
Merge branch 'master' into feat-code-actions
MikaelMayer Jul 1, 2022
02cd82a
Apply suggestions from code review
MikaelMayer Jul 18, 2022
e8cb5bb
Fixed warnings
MikaelMayer Jul 18, 2022
4f48b93
IEnumerable instead of arrays.
MikaelMayer Aug 5, 2022
a5d767f
Merge branch 'master' into feat-code-actions
MikaelMayer Aug 5, 2022
e9d574c
Fixed the merge commit.
MikaelMayer Aug 5, 2022
77e8085
Review 1
MikaelMayer Aug 9, 2022
29ab977
Merge branch 'master' into feat-code-actions
MikaelMayer Aug 9, 2022
af8ac08
Review comments
MikaelMayer Aug 10, 2022
06421ea
Review comments
MikaelMayer Aug 10, 2022
c962e0e
Merge branch 'master' into feat-code-actions
MikaelMayer Aug 10, 2022
274e314
Line check to avoid traversing all method.
MikaelMayer Aug 15, 2022
b8199cc
Fixed formatting warning
MikaelMayer Aug 25, 2022
92a029a
Merge branch 'master' into feat-code-actions
MikaelMayer Aug 25, 2022
71a42f6
Fixed the newline problem on windows machines.
MikaelMayer Aug 26, 2022
bba15f6
Merge branch 'master' into feat-code-actions
MikaelMayer Aug 26, 2022
44da9fe
Review comments
MikaelMayer Aug 26, 2022
d66b4d2
Update release notes
MikaelMayer Aug 26, 2022
5a1c545
Merge branch 'master' into feat-code-actions
MikaelMayer Aug 26, 2022
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Line check to avoid traversing all method.
  • Loading branch information
MikaelMayer committed Aug 15, 2022
commit 274e314a6d6dc0945b4d100c8daaae2f2c48294b
4 changes: 3 additions & 1 deletion Source/DafnyLanguageServer/Plugins/DafnyCodeActionHelpers.cs
Original file line number Diff line number Diff line change
Expand Up @@ -132,14 +132,16 @@ private static (Range? beforeEndBrace, string indentationExtra, string indentati
// Return the EndTok of them.
foreach (var module in program.Modules()) {
foreach (var topLevelDecl in module.TopLevelDecls) {
if (topLevelDecl is ClassDecl classDecl) {
if (topLevelDecl is ClassDecl classDecl && (classDecl.StartToken.line == 0 || classDecl.StartToken.Filename == documentUri && classDecl.StartToken.line <= line && line <= classDecl.EndToken.line)) {
foreach (var member in classDecl.Members) {
if (member is Method method && method.tok.filename == documentUri && method.Body != null &&
method.StartToken.line <= line && line <= method.EndToken.line &&
GetMatchingEndToken(line, col, method.Body) is { } token) {
return token;
}

if (member is Function { ByMethodBody: { } } function &&
function.StartToken.line <= line && line <= function.EndToken.line &&
GetMatchingEndToken(line, col, function.ByMethodBody) is { } token2) {
return token2;
}
Expand Down