From 2eb0f58bdd4059b5028c04e62ac47907341d43e4 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 12 Jan 2021 16:51:21 +0100 Subject: [PATCH] chore: restart worker only on didChange will otherwise be constantly retriggered by documentSymbol in Emacs --- src/Lean/Server/Watchdog.lean | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean index 14ff2ed8ec..97b1b573cb 100644 --- a/src/Lean/Server/Watchdog.lean +++ b/src/Lean/Server/Watchdog.lean @@ -260,13 +260,15 @@ section ServerM Messages that couldn't be sent can be queued up via the queueFailedMessage flag and will be discharged after the FileWorker is restarted. -/ def tryWriteMessage [Coe α JsonRpc.Message] (uri : DocumentUri) (msg : α) (writeAction : FileWorker → α → IO Unit) - (queueFailedMessage := true) : ServerM Unit := do + (queueFailedMessage := true) (restartCrashedWorker := false) : ServerM Unit := do let fw ← findFileWorker uri match fw.state with | WorkerState.crashed queuedMsgs => let mut queuedMsgs := queuedMsgs if queueFailedMessage then queuedMsgs := queuedMsgs.push msg + if !restartCrashedWorker then + return -- restart the crashed FileWorker eraseFileWorker uri startFileWorker fw.doc.meta @@ -325,7 +327,7 @@ section NotificationHandling else let newDoc : OpenDocument := ⟨newMeta, oldDoc.headerAst⟩ updateFileWorkers { fw with doc := newDoc } - tryWriteMessage doc.uri ⟨"textDocument/didChange", p⟩ FileWorker.writeNotification + tryWriteMessage doc.uri ⟨"textDocument/didChange", p⟩ FileWorker.writeNotification (restartCrashedWorker := true) def handleDidClose (p : DidCloseTextDocumentParams) : ServerM Unit := terminateFileWorker p.textDocument.uri