From 1b68daef397ac8792f08b0c193efec3e4ca2181e Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Fri, 13 Aug 2021 19:28:23 -0400 Subject: [PATCH] fix: clear messages earlier --- src/Lean/Server/FileWorker.lean | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index efc0befa95..6a1c287c54 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -85,8 +85,10 @@ section Elab the interrupt. Explicitly clearing diagnostics is difficult for a similar reason, because we cannot guarantee that no further diagnostics are emitted after clearing them. -/ - if snap.interactiveDiags.size > parentSnap.interactiveDiags.size then - publishDiagnostics m snap.diagnostics.toArray hOut + -- NOTE(WN): this is *not* redundent even if there are no new diagnostics in this snapshot + -- because empty diagnostics clear existing error/information squiggles. Therefore we always + -- want to publish in case there was previously a message at this position. + publishDiagnostics m snap.diagnostics.toArray hOut return snap /-- Elaborates all commands after `initSnap`, emitting the diagnostics into `hOut`. -/