Combine multi-message events into one larger event
The processing of a command such as debug auto on:
Lemma test : forall A B C : Prop,
(A -> B) ->
(B -> C) ->
(A -> C).
Proof.
debug auto.
yields the following in the language server debug log:
[lspManager , 759167, 1724680109.787295] sent: {
"params": {
"diagnostics": [
{
"message": "(* debug auto: *)",
"range": {
"end": { "character": 13, "line": 30 },
"start": { "character": 2, "line": 30 }
},
"severity": 3
},
{
"message": "* assumption. (*fail*)",
"range": {
"end": { "character": 13, "line": 30 },
"start": { "character": 2, "line": 30 }
},
"severity": 3
},
...
...
...
{
"message": "*** assumption. (*success*)",
"range": {
"end": { "character": 13, "line": 30 },
"start": { "character": 2, "line": 30 }
},
"severity": 3
}
],
},
"method": "textDocument/publishDiagnostics",
"jsonrpc": "2.0"
}
roughly 40 different messages from debug auto all pertaining to the same range and with the same severity
It might be nice and save some computation time if instead a single message/event was processed for commands that yield output related to a single range and with a single severity.
This additional API https://github.com/gares/sel/pull/16 should let one process feedback messages in batches.
It should be sufficient to use it here:
https://github.com/coq/vscoq/blob/95068b803143cf1d9a32d18dc70c2a4b571a446c/language-server/dm/executionManager.ml#L422
and modify the type of LocalFeedback to carry a list of stuff, eg
type feedback = Feedback.route_id * sentence_id * (Feedback.level * Loc.t option * Quickfix.t list * Pp.t)
...
| LocalFeedback of feedback Queue.t * feedback list