diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index cfb7aa50b0..50c316f991 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -131,7 +131,12 @@ section ServerM the interrupt. Explicitly clearing diagnostics is difficult for a similar reason, because we cannot guarantee that no further diagnostics are emitted after clearing them. -/ - sendDiagnostics snap.msgLog + sendDiagnostics <| snap.msgLog.add { + fileName := "" + pos := m.text.toPosition snap.endPos + severity := MessageSeverity.information + data := "processing..." + } snap | Sum.inr msgLog => sendDiagnostics msgLog