Diag channels #543
Merged
Diag channels #543
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
- Removed Info, Notice and Debug feedbacks from the standard diagnostics
- The feedback type encodes the channels in which the feedback will be displayed in the client - The accessor will be used in the lspManager to forward these feedbacks in a custom lsp verb
- PublishCoqFeedback and params in extProtocol
- CoqFeedback notification type - Seperate channels for each type of feedback (Debug, Info. Notice) - Appends the results in the corresponding channels
- Seperated tests in feedbacks (Notice, Info, Debug) and diagnostics (Error, Warning)
|
I am still not sure if this is the right way to go @maximedenes.
How do we reconcile the two ? This PR aims at throwing Debug | Info | Notice into their own dedicated channels in the extension and Warning | Error in the usual Problems channel. Maybe at least the separation should be clearer in the backend. What do you think ? |
Yes, I think the distinction should be clear: only Error and Warning should be emitted as diagnostics (for now). Notice & Info feedback should be collected by the server and sent for display to the dedicated channels. I'm not sure about Debug, but we can see that later. |
- Seperated CoqFeedback types and Diagnostics types more clearly - Changed the diagnostics function to a feedbacks_and_diagnostics function - Reworked the code and the tests to take that into account
maximedenes
approved these changes
Aug 4, 2023
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Appending the different types of coq feedbacks (Debug, Info, Notice) in separate channels instead of treating them as diagnostics