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

Added interface for plugins to add JsonRpcRequestHandlers to the language server #5161

Merged
merged 8 commits into from
May 14, 2024

Conversation

BurstingF
Copy link
Contributor

Description

This change will add an interface for plugins to add request handlers to the Dafny language server, which allows plugins to provide more features than just code actions.

How has this been tested?

Test has been added to DafnyLanguageServer.Test in a similar way to how a test for GetDafnyCodeActionProviders() was added.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

@atomb atomb requested a review from MikaelMayer March 7, 2024 22:27
Copy link
Member

@atomb atomb left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This looks pretty good to me, and I like how simple it is. I'd like to know what @MikaelMayer, who originally set up the LSP plugin mechanism thinks about it, too, though.

Copy link
Member

@MikaelMayer MikaelMayer left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is a great addition that I guess will enable to extend the language server a bit more.
Could you also please add relevant documentation about that new feature?
https://dafny.org/latest/DafnyRef/DafnyRef#sec-plugins
The file is here (feel free to also perform enhancements in the presentation, as needed)
docs\DafnyRef\Plugins.md

Last but not least, please add an item named 5161.feat here:
docs\dev\news
it should contain a summary of the feature that will be used for the release notes. Feel free to look at others elements for inspiration.

After all of this, I guess we can merge. Thanks for your contribution!

@BurstingF BurstingF requested a review from MikaelMayer March 8, 2024 09:54
Copy link
Member

@MikaelMayer MikaelMayer left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The documentation is great! Thank you very much for the effort putting it altogether.
A few minor suggested upgrades left on the newly added content and this is good to go.

docs/DafnyRef/Plugins.md Outdated Show resolved Hide resolved
docs/dev/news/5161.feat Outdated Show resolved Hide resolved
docs/DafnyRef/Plugins.md Outdated Show resolved Hide resolved
docs/DafnyRef/Plugins.md Outdated Show resolved Hide resolved
docs/DafnyRef/Plugins.md Outdated Show resolved Hide resolved
docs/DafnyRef/Plugins.md Outdated Show resolved Hide resolved
docs/DafnyRef/Plugins.md Outdated Show resolved Hide resolved
@BurstingF
Copy link
Contributor Author

Thanks for the suggestions, I've implemented them and a few other minor improvements in f1166f3

@BurstingF BurstingF requested a review from MikaelMayer March 9, 2024 12:59
MikaelMayer
MikaelMayer previously approved these changes Mar 21, 2024
@MikaelMayer MikaelMayer enabled auto-merge (squash) March 21, 2024 14:31
auto-merge was automatically disabled March 27, 2024 15:17

Head branch was pushed to by a user without write access

@wstomv
Copy link

wstomv commented May 14, 2024

Hello Dafny Developers,

@BurstingF is doing a CS Master project at Eindhoven University of Technology, Netherlands, where a VS code plugin is developed that offers more advanced refactoring and other Dafny support features. It would be helpful if this pull request would be honored, so that our plugin under development can use the official plugin, and in particular its Dafny Language Server. Otherwise, our plugin will have to install its own Dafny Language Server, which adds weight and overhead. In the future, it is imaginable that some features of our plugin (after it has been tested and proven useful) can be ported to the official plugin. Thanks for your consideration.

If further work on our side on this PR is needed, then it would be good to hear concretely what work is still expected from us.

@keyboardDrummer keyboardDrummer enabled auto-merge (squash) May 14, 2024 13:21
Copy link
Member

@keyboardDrummer keyboardDrummer left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM. Apologies for the delay in merging this.

@keyboardDrummer keyboardDrummer merged commit 8da3ddd into dafny-lang:master May 14, 2024
21 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

5 participants