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

Combine multi-message events into one larger event #878

Open
Durbatuluk1701 opened this issue Aug 26, 2024 · 2 comments
Open

Combine multi-message events into one larger event #878

Durbatuluk1701 opened this issue Aug 26, 2024 · 2 comments
Labels
enhancement New feature or request

Comments

@Durbatuluk1701
Copy link
Contributor

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request
Projects
None yet
Development

No branches or pull requests

4 participants
@rtetley @Durbatuluk1701 and others