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

[Feature request]: Documentation on hover #3024

Open
MikaelMayer opened this issue Nov 8, 2022 · 0 comments
Open

[Feature request]: Documentation on hover #3024

MikaelMayer opened this issue Nov 8, 2022 · 0 comments
Labels
kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: language server Support for LSP in Dafny (server part; client is in ide-vscode repo)

Comments

@MikaelMayer
Copy link
Member

What is the feature you would like to see in a future version of Dafny?

I would like to have a place in the code to put my documentation, and when I hover over a function in my codebase, that documentation would be shown in my IDE.

Design suggestions

  • Create an opinionated .DocString field on top-level declarations so that this docstring is available by API calls.
  • This docstring should be raw (not contain the comment signs /* */ or //)
  • It should be possible to modify this docstring via a plugin, e.g. to format it.
  • Since we use VSCode, by default we can have docstring formatted in VSCode's markdown.
@keyboardDrummer keyboardDrummer added kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: language server Support for LSP in Dafny (server part; client is in ide-vscode repo) labels Nov 9, 2022
@keyboardDrummer keyboardDrummer added this to the Standard IDE features milestone Nov 9, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: language server Support for LSP in Dafny (server part; client is in ide-vscode repo)
Projects
None yet
Development

No branches or pull requests

2 participants