From 21474b6d06a71b2165aa27cfd040a1ff893aa6e7 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Tue, 6 Oct 2020 15:06:26 +0200 Subject: [PATCH] feat: dedicated tasks for forwarding --- src/Lean/Server/Watchdog.lean | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean index 310252745a..c748eef792 100644 --- a/src/Lean/Server/Watchdog.lean +++ b/src/Lean/Server/Watchdog.lean @@ -186,7 +186,7 @@ def fwdMsgTask (fw : FileWorker) : ServerM (Task WorkerEvent) := fun st => (Task.map (fun either => match either with | Except.ok ev => ev - | Except.error e => WorkerEvent.crashed e)) <$> (IO.asTask $ fwdMsgAux fw st.hOut ()) + | Except.error e => WorkerEvent.crashed e)) <$> (IO.asTask (fwdMsgAux fw st.hOut ()) Task.Priority.dedicated) private def parsedImportsEndPos (input : String) : IO String.Pos := do emptyEnv ← mkEmptyEnvironment; @@ -351,15 +351,14 @@ partial def mainLoop : Unit → ServerM Unit - client sends us a message - a worker does something -/ clientTask ← liftIO $ IO.asTask $ ServerEvent.ClientMsg <$> readLspMessage st.hIn; - let clientTask := Task.map + let clientTask := clientTask.map (fun either => match either with | Except.ok ev => ev - | Except.error e => ServerEvent.ClientError e) - clientTask; + | Except.error e => ServerEvent.ClientError e); let workerTasks := workers.fold (fun acc uri fw => - Task.map (ServerEvent.WorkerEvent uri fw) fw.commTask :: acc) + fw.commTask.map (ServerEvent.WorkerEvent uri fw) :: acc) ([] : List (Task ServerEvent)); ev ← liftIO $ IO.waitAny $ clientTask :: workerTasks;