feat: watchdog: show message while worker is starting

src/Lean/Server/FileWorker.lean

@@ -94,21 +94,6 @@ end Utils
 
 /- Asynchronous snapshot elaboration. -/
 section Elab
-  def publishDiagnostics (m : DocumentMeta) (diagnostics : Array Lsp.Diagnostic) (hOut : FS.Stream) : IO Unit :=
-    hOut.writeLspNotification {
-      method := "textDocument/publishDiagnostics"
-      param  := {
-        uri         := m.uri
-        version?    := m.version
-        diagnostics := diagnostics
-        : PublishDiagnosticsParams
-      }
-    }
-
-  def publishMessages (m : DocumentMeta) (msgLog : MessageLog) (hOut : FS.Stream) : IO Unit := do
-    let diagnostics ← msgLog.msgs.mapM (msgToDiagnostic m.text)
-    publishDiagnostics m diagnostics.toArray hOut
-
   /-- Elaborates the next command after `parentSnap` and emits diagnostics into `hOut`. -/
   private def nextCmdSnap (m : DocumentMeta) (parentSnap : Snapshot) (cancelTk : CancelToken) (hOut : FS.Stream)
   : ExceptT ElabTaskError IO Snapshot := do

src/Lean/Server/Utils.lean

@@ -121,6 +121,21 @@ def foldDocumentChanges (changes : @& Array Lsp.TextDocumentContentChangeEvent)
   -- NOTE: We assume Lean files are below 16 EiB.
   changes.foldl accumulateChanges (oldText, 0xffffffff)
 
+def publishDiagnostics (m : DocumentMeta) (diagnostics : Array Lsp.Diagnostic) (hOut : FS.Stream) : IO Unit :=
+  hOut.writeLspNotification {
+    method := "textDocument/publishDiagnostics"
+    param  := {
+      uri         := m.uri
+      version?    := m.version
+      diagnostics := diagnostics
+      : PublishDiagnosticsParams
+    }
+  }
+
+def publishMessages (m : DocumentMeta) (msgLog : MessageLog) (hOut : FS.Stream) : IO Unit := do
+  let diagnostics ← msgLog.msgs.mapM (msgToDiagnostic m.text)
+  publishDiagnostics m diagnostics.toArray hOut
+
 end Lean.Server
 
 namespace List

src/Lean/Server/Watchdog.lean

@@ -229,6 +229,7 @@ section ServerM
       | Except.error e => WorkerEvent.ioError e
 
   def startFileWorker (m : DocumentMeta) : ServerM Unit := do
+    publishDiagnostics m #[{ range := ⟨⟨0, 0⟩, ⟨0, 0⟩⟩, severity? := DiagnosticSeverity.information, message := "starting new server for file..." }] (← read).hOut
     let st ← read
     let headerAst ← parseHeaderAst m.text.source
     let workerProc ← Process.spawn {