Improve code navigation for unreferenced declaration #5483
Conversation
keyboardDrummer
changed the title
| @@ -1,10 +1,11 @@ | |||
| using System.Collections.Generic; | |||
| using System.Diagnostics.Contracts; | |||
| using System.Linq; | |||
| using OmniSharp.Extensions.LanguageServer.Protocol.Models; | |||
There was a problem hiding this comment.
I'm a little sad to have the DafnyCore package depend on LSP-specific stuff, but I think the tradeoff is probably worth it.
There was a problem hiding this comment.
Looking more closely, I see that isn't a new dependency, so it's even more on the side of being worth it.
There was a problem hiding this comment.
I think it's to be expected that a compiler will have a public interface so it can be used as a library, and LSP happens to already contain many types that are useful for this interface, such as Position and Range, and used in this file, SymbolKind. I've made this PR to reduce what's in scope from DafnyCore: #5502
| @@ -197,6 +198,11 @@ public TypeParameter(RangeToken tok, Name name, int positionalIndex, ParentType | |||
| } | |||
| } | |||
|
|
|||
| public override SymbolKind? Kind => SymbolKind.TypeParameter; | |||
| public override string GetDescription(DafnyOptions options) { | |||
| return null; // TODO test the effect of this | |||
There was a problem hiding this comment.
I'm not sure how to interpret this comment. Have you tested calling GetDescription on a TypeParameter?
Description
IHasUsagestoIHasReferences, to be more in line with LSP namingIDeclarationOrUsagetoIHasNavigationToken, and its memberNameTokentoNavigationTokenrequest.Context.IncludeDeclarationvalue of the LSP references requestHow has this been tested?
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.