max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: dedicated tasks for forwarding

Browse source
This commit is contained in:
Marc Huisinga 2020-10-06 15:06:26 +02:00 • committed by Sebastian Ullrich
parent d433fe58af
commit 21474b6d06
1 changed files with 4 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/Lean/Server/Watchdog.lean
View file

@ -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;