Skip to content

Prevent unnecessary diagnostics from being sent to the IDE client #4377

Open
@keyboardDrummer

Description

@keyboardDrummer

See test ResolutionDiagnosticsAreKeptWhenNonEdgeCrossingChangesAreMade for more information

Implementation hints

NotificationPublisher.publishedDiagnostics is currently not migrated, that's why the equality check fails and these parse diagnostics are sent. Instead, there should be a single client state for the entire server, which is updated by a Compilation

Metadata

Metadata

Assignees

No one assigned

    Labels

    area: performancePerformance issuespart: language serverSupport for LSP in Dafny (server part; client is in ide-vscode repo)

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions