Skip to content

Commit 3622e15

Browse files
committed
fix: remove version handling
1 parent a7ffb3a commit 3622e15

File tree

1 file changed

+1
-13
lines changed

1 file changed

+1
-13
lines changed

vscode-lean4/src/diagnostics.ts

Lines changed: 1 addition & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -40,19 +40,10 @@ export class LeanClientDiagnosticCollection implements Disposable {
4040
private static determineChangeKind(
4141
prev: LeanPublishDiagnosticsParams | undefined,
4242
next: LeanPublishDiagnosticsParams,
43-
): DiagnosticChangeKind | 'drop' {
43+
): DiagnosticChangeKind {
4444
if (prev === undefined) {
4545
return 'replace'
4646
}
47-
if (next.version === undefined || prev.version === undefined) {
48-
return 'replace'
49-
}
50-
if (next.version > prev.version) {
51-
return 'replace'
52-
}
53-
if (next.version < prev.version) {
54-
return 'drop'
55-
}
5647
if (!next.isIncremental) {
5748
return 'replace'
5849
}
@@ -62,9 +53,6 @@ export class LeanClientDiagnosticCollection implements Disposable {
6253
publishDiagnostics(params: LeanPublishDiagnosticsParams): void {
6354
const prev = this.diags.get(params.uri)
6455
const kind = LeanClientDiagnosticCollection.determineChangeKind(prev, params)
65-
if (kind === 'drop') {
66-
return
67-
}
6856

6957
let accumulated: LeanDiagnostic[]
7058
if (kind === 'append') {

0 commit comments

Comments
 (0)