From 8e3052fe8dc554c397ed337b0c2d2eb0fe758cd1 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 30 Dec 2020 21:59:40 +0100
Subject: [PATCH] feat: server: show "processing..." message

---
 src/Lean/Server/FileWorker.lean | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

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 := "<ignored>"
+        pos      := m.text.toPosition snap.endPos
+        severity := MessageSeverity.information
+        data     := "processing..."
+      }
       snap
     | Sum.inr msgLog =>
       sendDiagnostics msgLog