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: Hover in language server display documentation #2364

Closed
wants to merge 34 commits into from

Conversation

MikaelMayer
Copy link
Member

@MikaelMayer MikaelMayer commented Jul 5, 2022

This PR makes it possible to hover over a symbol and not only see the signature of the declaration, but also the comment that precedes it.
Any comment in /** */ or /// will be visualized as plain markdown.
If this comment is detected to have a subset of the JavaDoc format, it is formatted as such.

No change to the IDE extension is required.

Screenshots
On functions
image
image

On fields
image
image

Unformatted comments:
image
image

The most relevant test is here and test comments on constants, fields, methods, functions, lemmas, predicates, least predicates, twostate lemmas...
https://github.com/dafny-lang/dafny/pull/1801/files#diff-1edc7ab0bf5b3c02cf78f59e65636710aeaf47a0a5e37f889a3c364a5cf207b5R432

Implementation details

  • Update the LSP's hover handler so that it can also output rich formatted comments by "parsing" javadoc comments.
  • The hover tests sources are now also valid Dafny files, so that it makes it easier to manually test and debug in the IDE.

To review:

  • Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs The main place where Dafny computes the hovering content
  • Source/DafnyLanguageServer.Test/Lookup/HoverTest.cs Refactored all the tests to have an executable source, and added the final hover test
  • Source/DafnyLanguageServer/Language/Symbols/ClassSymbol.cs Added a Token to every symbol, this is an example
  • Source/DafnyLanguageServer/Language/Symbols/DataTypeSymbol.cs Added a Token to every symbol, this is an example
  • Source/DafnyLanguageServer/Language/Symbols/FieldSymbol.cs Same
  • Source/DafnyLanguageServer/Language/Symbols/FunctionSymbol.cs Same
  • Source/DafnyLanguageServer/Language/Symbols/ILocalizableSymbol.cs This is where I require that localizable symbols have a token. This token is not necessarily the position of the symbol, it's where its comment is.
  • Source/DafnyLanguageServer/Language/Symbols/MethodSymbol.cs a symbol with a token
  • Source/DafnyLanguageServer/Language/Symbols/ModuleSymbol.cs same
  • Source/DafnyLanguageServer/Language/Symbols/ScopeSymbol.cs same
  • Source/DafnyLanguageServer/Language/Symbols/TypeWithMembersSymbolBase.cs same
  • Source/DafnyLanguageServer/Language/Symbols/ValueTypeSymbol.cs same
  • Source/DafnyLanguageServer/Language/Symbols/VariableSymbol.cs same

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

MikaelMayer and others added 30 commits February 8, 2022 11:36
# Conflicts:
#	Source/Dafny.sln
#	Source/Dafny/AST/DafnyAst.cs
#	Source/Dafny/Resolver.cs
#	Source/Directory.Build.props
#	Test/libraries
# Conflicts:
#	Source/Dafny/Verifier/Translator.ClassMembers.cs
#	Source/Dafny/Verifier/Translator.cs
# Conflicts:
#	RELEASE_NOTES.md
#	Source/DafnyLanguageServer.Test/Lookup/HoverTest.cs
This reverts commit 45e661a.
@MikaelMayer MikaelMayer marked this pull request as draft July 5, 2022 20:34
@MikaelMayer
Copy link
Member Author

Closed in favor of #3756

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.

1 participant