Feat: Auto-completion of @-attributes for the language server #5846
Conversation
| InsertText = attributeName, // TODO: Parentheses | ||
| Detail = "" // TODO: Details of attribute name |
There was a problem hiding this comment.
These look more like unfinished PR todos rather than planned improvements for the next iteration
There was a problem hiding this comment.
I'm actually going to create a new PR for these todos and added empty details for now, and just attribute name to be inserted. The inserted name is probably not going to change since I don't know how to instruct VSCode to place the caret inside parentheses. But the details about showing up argument names, types and default value is much more complicated than I though (e.g. for fuel, the high fuel should be low fuel + 1 by default) and needs to be thoroughly tested. Let's do one thing at a time.
| @@ -86,11 +93,81 @@ public CompletionList Process() { | |||
| return new CompletionList(); | |||
| } | |||
|
|
|||
| private string GetLastTwoCharactersBeforePositionIncluded(TextReader fileContent, DafnyPosition position) { | |||
There was a problem hiding this comment.
I would think this would be a lot simpler if you located the index of the current position and then grabbed the previous two characters. It doesn't seem like processing anything line-by-line buys you anything - "\n@" will still be processed correctly since \n is whitespace.
| if (projectManager == null) { | ||
| return false; | ||
| } | ||
| var fileContent = projectManager.ReadFile(request.TextDocument.Uri.ToUri()); |
There was a problem hiding this comment.
Reading the whole file doesn't scale for large files. Please use already processed file contents where the relevant location can be found in O(1) time.
There was a problem hiding this comment.
I'll get back to this soon, but meantime, do you have a hint about where the already processed file contents is? I thought ReadFile would just give me the current string
There was a problem hiding this comment.
I've pushed a commit Use a TextBuffer instead of a FileReader, that addresses this comment.
There was a problem hiding this comment.
Do you know why your commit breaks some tests? For example:
Could not close file file:///tmp/z3sq5jsc.kyh/DocumentStaysUnloadedWhenClosed.dfy because it was not open.
|
|
||
| private CompletionList CreateAtAttributeCompletionList() { | ||
| var completionItems = | ||
| Attributes.BuiltinAtAttributes.Select(b => |
There was a problem hiding this comment.
Shouldn't this be filtered to the part of the attribute that is already typed? Or are you only providing code completion upon writing the @, but not afterwards?
There was a problem hiding this comment.
I'm only providing instant code completion upon writing the @, not afterwards. The IDE will then filter the list according to what is being typed.
| @@ -126,6 +127,10 @@ public ProjectManager( | |||
|
|
|||
| private const int MaxRememberedChanges = 100; | |||
|
|
|||
| public TextReader ReadFile(Uri fileToRead) { | |||
There was a problem hiding this comment.
This method here makes no sense to me. Why not use a filesystem directly?
There was a problem hiding this comment.
Your update for reading the last two characters forgot the test case when the position is given in line zero but the column is the number of characters. That fails the test slowlytypefile
There was a problem hiding this comment.
I added a fix for slowlytypefile
Description
This PR adds the ability for detecting that the user presses @ when after a space, which is the signature of an attribute. It then provides auto-complete of the attribute name.
How has this been tested?
Tests added in DafnyLanguageServer.Tests
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.