max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: clear messages earlier

Browse source
This commit is contained in:
Wojciech Nawrocki 2021-08-13 19:28:23 -04:00 • committed by Leonardo de Moura
parent feff4c2ed3
commit 1b68daef39
1 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Lean/Server/FileWorker.lean
View file

@ -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`. -/