coq / vscoq

Visual Studio Code extension for Coq
MIT License
335 stars 68 forks source link

Combine multi-message events into one larger event #878

Open Durbatuluk1701 opened 1 month ago

Durbatuluk1701 commented 1 month ago

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.