diff --git a/src/Lean/Server/AsyncList.lean b/src/Lean/Server/AsyncList.lean
new file mode 100644
index 0000000000..8389907d8e
--- /dev/null
+++ b/src/Lean/Server/AsyncList.lean
@@ -0,0 +1,109 @@
+#lang lean4
+/-
+Copyright (c) 2020 Wojciech Nawrocki. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Authors: Wojciech Nawrocki
+-/
+import Init.System.IO
+
+namespace IO
+
+universes u v
+
+/-- An async IO list is like a lazy list but instead of being *unevaluated* `Thunk`s,
+lazy tails are `Task`s *being evaluated asynchronously*. A tail can signal the end
+of computation (successful or due to a failure) with a terminating value of type `ε`. -/
+inductive AsyncList (ε : Type u) (α : Type v)
+| cons (hd : α) (tl : AsyncList ε α)
+| asyncCons (hd : α) (tl : Task $ Except ε $ AsyncList ε α)
+| nil
+
+namespace AsyncList
+
+-- TODO(WN): IO doesn't like universes :(
+variables {α : Type} {ε : Type}
+
+instance inhabited : Inhabited (AsyncList ε α) := ⟨nil⟩
+
+-- TODO(WN): tail-recursion without forcing sync?
+partial def append : AsyncList ε α → AsyncList ε α → AsyncList ε α
+  | cons hd tl, s => cons hd (append tl s)
+  | asyncCons hd ttl, s => asyncCons hd (ttl.map $ Except.map (append · s))
+  | nil, s => s
+
+instance : HasAppend (AsyncList ε α) := ⟨append⟩
+
+def ofList : List α → AsyncList ε α :=
+  List.foldr AsyncList.cons AsyncList.nil
+
+instance : Coe (List α) (AsyncList ε α) := ⟨ofList⟩
+
+/-- Given a step computation `f` which takes the accumulator and either produces
+another value or stops with a terminating value, produces an async stream of its
+iterated applications. The computation can throw IO exceptions, so to handle this
+the terminating value type must include `IO.Error`.
+
+Optionally, a specified computation can be ran on task cancellation.
+An alternative for cooperative concurrency is to check this in `f`. -/
+partial def unfoldAsync [Coe Error ε] (f : α → ExceptT ε IO α)
+  (init : α) (onCanceled : Option (α → IO ε) := none)
+: IO (AsyncList ε α) := do
+  let coeErr (t : Task $ Except Error $ Except ε $ AsyncList ε α) : Task (Except ε $ AsyncList ε α) :=
+    t.map (fun
+      | Except.ok v              => v
+      | Except.error (e : Error) => Except.error (e : ε))
+
+  let rec step (a : α) : ExceptT ε IO (AsyncList ε α) := do
+    if onCanceled.isSome ∧ (← checkCanceled) then
+      throw (← onCanceled.get! a)
+    else
+      let aNext ← f a
+      let tNext ← coeErr <$> asTask (step aNext)
+      return asyncCons aNext tNext
+
+  let tInit ← coeErr <$> asTask (step init)
+  asyncCons init tInit
+
+/-- Waits for the entire computation to finish and returns the computed
+list. If computation was ongoing, also returns the terminating value. -/
+partial def waitAll : AsyncList ε α → List α × Option ε
+  | cons hd tl =>
+    let ⟨l, e?⟩ := tl.waitAll
+    ⟨hd :: l, e?⟩
+  | nil => ⟨[], none⟩
+  | asyncCons hd tl =>
+    match tl.get with
+    | Except.ok tl =>
+      let ⟨l, e?⟩ := tl.waitAll
+      ⟨hd :: l, e?⟩
+    | Except.error e => ⟨[hd], some e⟩
+
+/-- Extends the `finishedPrefix` as far as possible. If computation was ongoing
+and has finished, also returns the terminating value. -/
+partial def updateFinishedPrefix : AsyncList ε α → IO (AsyncList ε α × Option ε)
+  | cons hd tl => do
+    let ⟨tl, e?⟩ ← tl.updateFinishedPrefix
+    pure ⟨cons hd tl, e?⟩
+  | nil => pure ⟨nil, none⟩
+  | l@(asyncCons hd tl) => do
+    if (← hasFinished tl) then
+      match tl.get with
+      | Except.ok tl =>
+        let ⟨tl, e?⟩ ← tl.updateFinishedPrefix
+        pure ⟨cons hd tl, e?⟩
+      | Except.error e => pure ⟨cons hd nil, some e⟩
+    else pure ⟨l, none⟩
+
+private partial def finishedPrefixAux : List α → AsyncList ε α → List α
+  | acc, cons hd tl      => finishedPrefixAux (hd :: acc) tl
+  | acc, nil             => []
+  | acc, asyncCons hd tl => []
+
+/-- The longest already-computed prefix of the stream. -/
+def finishedPrefix : AsyncList ε α → List α :=
+  List.reverse ∘ (finishedPrefixAux [])
+
+end AsyncList
+
+end IO
diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean
index 2c2acf66a7..e7af899ba4 100644
--- a/src/Lean/Server/FileWorker.lean
+++ b/src/Lean/Server/FileWorker.lean
@@ -12,6 +12,7 @@ import Lean.Server.Snapshots
 import Lean.Server.Utils
 import Lean.Data.Lsp
 import Lean.Data.Json.FromToJson
+import Lean.Server.AsyncList
 
 /-!
 For general server architecture, see `README.md`. For details of IPC communication, see `Watchdog.lean`.
@@ -48,7 +49,7 @@ diagnostics ← log.msgs.mapM (msgToDiagnostic text);
 Lsp.writeLspNotification h "textDocument/publishDiagnostics"
   { uri         := uri,
     version?    := version,
-    diagnostics := diagnostics.toArray 
+    diagnostics := diagnostics.toArray
     : PublishDiagnosticsParams }
 
 private def logSnapContent (s : Snapshot) (text : FileMap) : IO Unit :=
@@ -59,85 +60,37 @@ inductive TaskError
 | eof
 | ioError (e : IO.Error)
 
-inductive ElabTask
-| mk (snap : Snapshot) (next : Task (Except TaskError ElabTask)) : ElabTask
+instance : Coe IO.Error TaskError := ⟨TaskError.ioError⟩
 
-namespace ElabTask
-
-private def runTask (act : IO (Except TaskError ElabTask)) : IO (Task (Except TaskError ElabTask)) := do
-t ← asTask act;
-pure $ t.map $ fun error => 
-  match error with
-  | Except.ok e => e
-  | Except.error ioError => Except.error (TaskError.ioError ioError)
-
-private partial def runCore (h : FS.Stream) (uri : DocumentUri) (version : Nat) (contents : FileMap) 
-  : Snapshot → IO (Except TaskError ElabTask)
-| parent => do
-  result ← compileNextCmd contents.source parent;
-  match result with
+private def nextCmdSnap (h : FS.Stream) (uri : DocumentUri) (version : Nat) (contents : FileMap)
+  : Snapshot → ExceptT TaskError IO Snapshot
+| parentSnap => do
+  maybeSnap ← monadLift $ compileNextCmd contents.source parentSnap;
+  match maybeSnap with
   | Sum.inl snap => do
-    -- TODO(MH): check for interrupt with increased precision
-    canceled ← checkCanceled;
-    if canceled then
-      pure (Except.error TaskError.aborted)
-    else do
-      -- NOTE(MH): This relies on the client discarding old diagnostics upon receiving new ones
-      -- while prefering newer versions over old ones. The former is necessary because we do
-      -- not explicitly clear older diagnostics, while the latter is necessary because we do
-      -- not guarantee that diagnostics are emitted in order. Specifically, it may happen that
-      -- we interrupted this elaboration task right at this point and a newer elaboration task
-      -- emits diagnostics, after which we emit old diagnostics because we did not yet detect
-      -- 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 h uri version contents snap.msgLog;
-      t ← runTask (runCore snap);
-      pure (Except.ok ⟨snap, t⟩)
+    -- NOTE(MH): This relies on the client discarding old diagnostics upon receiving new ones
+    -- while prefering newer versions over old ones. The former is necessary because we do
+    -- not explicitly clear older diagnostics, while the latter is necessary because we do
+    -- not guarantee that diagnostics are emitted in order. Specifically, it may happen that
+    -- we interrupted this elaboration task right at this point and a newer elaboration task
+    -- emits diagnostics, after which we emit old diagnostics because we did not yet detect
+    -- the interrupt. Explicitly clearing diagnostics is difficult for a similar reason,
+    -- because we cannot guarantee that no further diagnostics are emitted after clearing
+    -- them.
+    monadLift $ sendDiagnostics h uri version contents snap.msgLog;
+    pure snap
   | Sum.inr msgLog => do
-    canceled ← checkCanceled;
-    if canceled then
-      pure (Except.error TaskError.aborted)
-    else do
-      sendDiagnostics h uri version contents msgLog;
-      pure (Except.error TaskError.eof)
+    monadLift $ sendDiagnostics h uri version contents msgLog;
+    throw TaskError.eof
 
-def run (h : FS.Stream) (uri : DocumentUri) (version : Nat) (contents : FileMap) (parent : Snapshot) 
-  : IO ElabTask := do
-t ← runTask (runCore h uri version contents parent);
-pure ⟨parent, t⟩
-
-partial def branchOffAt (h : FS.Stream) (uri : DocumentUri) (version : Nat) (contents : FileMap) 
-  : ElabTask → String.Pos → IO ElabTask
-| ⟨snap, nextTask⟩, changePos => do
-  finished ← hasFinished nextTask;
-  if finished then
-    match nextTask.get with
-    | Except.ok (next@⟨nextSnap, _⟩) => do
-       -- if next contains the change ...
-       -- (it will never be the header snap because the
-       -- watchdog will never send didChange notifs with
-       -- header changes to the file worker)
-       if changePos ≤ nextSnap.endPos then
-         -- we do not need to cancel the old task explicitly since tasks without refs are marked as cancelled 
-         -- by the GC
-         run h uri version contents snap
-       else do
-         newNext ← branchOffAt next changePos;
-         pure ⟨snap, Task.pure (Except.ok newNext)⟩
-    | Except.error e => 
-      match e with
-      -- this case should not be possible. only the main task aborts tasks and ensures that aborted tasks
-      -- do not show up in `snapshots` of EditableDocument below.
-      | TaskError.aborted => throwServerError 
-        "Internal server error: reached case that should not be possible during server file worker task branching"
-      | TaskError.eof => run h uri version contents snap
-      | TaskError.ioError ioError => throw ioError
-  else
-    -- we do not need to cancel the old task explicitly since tasks without refs are marked as cancelled by the GC
-    run h uri version contents snap
-
-end ElabTask
+def unfoldCmdSnaps (h : FS.Stream) (uri : DocumentUri) (version : Nat) (contents : FileMap)
+  (initSnap : Snapshot)
+: IO (AsyncList TaskError Snapshot) :=
+  AsyncList.unfoldAsync
+    (nextCmdSnap h uri version contents)
+    initSnap
+    -- TODO(MH): check for interrupt with increased precision
+    (some fun _ => pure TaskError.aborted)
 
 /-- A document editable in the sense that we track the environment
 and parser state after each command so that edits can be applied
@@ -145,8 +98,10 @@ without recompiling code appearing earlier in the file. -/
 structure EditableDocument :=
 (version : Nat)
 (text : FileMap)
+/- The first snapshot is that after the header. -/
+(headerSnap : Snapshot)
 /- Subsequent snapshots occur after each command. -/
-(snapshots : ElabTask)
+(cmdSnaps : AsyncList TaskError Snapshot)
 
 namespace EditableDocument
 
@@ -155,21 +110,37 @@ open Elab
 /-- Compiles the contents of a Lean file. -/
 def compileDocument (h : FS.Stream) (uri : DocumentUri) (version : Nat) (text : FileMap) : IO EditableDocument := do
 headerSnap ← Snapshots.compileHeader text.source;
-task ← ElabTask.run h uri version text headerSnap;
-pure ⟨version, text, task⟩
+cmdSnaps ← unfoldCmdSnaps h uri version text headerSnap;
+pure ⟨version, text, headerSnap, cmdSnaps⟩
 
 /-- Given `changePos`, the UTF-8 offset of a change into the pre-change source,
 and the new document, updates editable doc state. -/
-def updateDocument (h : FS.Stream) (uri : DocumentUri) (doc : EditableDocument) (changePos : String.Pos) 
-  (newVersion : Nat) (newText : FileMap) : IO EditableDocument :=
--- The watchdog only restarts the file worker when the syntax tree of the header changes.
--- If e.g. a newline is deleted, it will not restart this file worker, but we still
--- need to reparse the header so the offsets are correct.
-match doc.snapshots with
-| ⟨headerSnap, next⟩ => do
-  newHeaderSnap ← reparseHeader newText.source headerSnap;
-  newSnapshots ← (ElabTask.mk newHeaderSnap next).branchOffAt h uri newVersion newText changePos;
-  pure ⟨newVersion, newText, newSnapshots⟩
+def updateDocument (h : FS.Stream) (uri : DocumentUri) (doc : EditableDocument) (changePos : String.Pos)
+  (newVersion : Nat) (newText : FileMap) : IO EditableDocument := do
+  -- The watchdog only restarts the file worker when the syntax tree of the header changes.
+  -- If e.g. a newline is deleted, it will not restart this file worker, but we still
+  -- need to reparse the header so the offsets are correct.
+  newHeaderSnap ← reparseHeader newText.source doc.headerSnap;
+
+  ⟨cmdSnaps, e?⟩ ← doc.cmdSnaps.updateFinishedPrefix;
+  match e? with
+  -- this case should not be possible. only the main task aborts tasks and ensures that aborted tasks
+  -- do not show up in `snapshots` of EditableDocument below.
+  | some TaskError.aborted => throwServerError
+    "Internal server error: reached case that should not be possible during server file worker task branching"
+  | some (TaskError.ioError ioError) => throw ioError
+  | _ => do -- No error or EOF
+    -- NOTE(WN): endPos is greedy in that it consumes input until the next token,
+    -- so a change on some whitespace after a command recompiles it. We could
+    -- be more precise.
+    let validSnaps := cmdSnaps.finishedPrefix.takeWhile (fun s => s.endPos < changePos);
+    -- NOTE: the watchdog never sends didChange notifs with a header change to the
+    -- worker, so the header snapshot is always valid.
+    let lastSnap := validSnaps.getLastD doc.headerSnap;
+    newSnaps ← unfoldCmdSnaps h uri newVersion newText lastSnap;
+    let newCmdSnaps := AsyncList.ofList validSnaps ++ newSnaps;
+    -- NOTE: We do not cancel old tasks explicitly, the GC does this for us when no refs remain.
+    pure ⟨newVersion, newText, newHeaderSnap, newCmdSnaps⟩
 
 end EditableDocument
 
@@ -245,7 +216,7 @@ match method with
 | "$/cancelRequest"        => h CancelParams handleCancelRequest
 | _                        => throwServerError $ "Got unsupported notification method: " ++ method
 
-def queueRequest {α : Type*} (id : RequestID) (handler : α → EditableDocument → IO Unit) (params : α) 
+def queueRequest {α : Type*} (id : RequestID) (handler : α → EditableDocument → IO Unit) (params : α)
   : ServerM Unit := do
 doc ← getDocument;
 requestTask ← monadLift $ asTask (handler params doc);
@@ -300,8 +271,8 @@ _ ← IO.setStderr e; -- TODO(WN): use a stream var in WorkerM instead of global
 doc ← openDocument o param;
 docRef ← IO.mkRef doc;
 pendingRequestsRef ← IO.mkRef (RBMap.empty : PendingRequestMap);
-runReader (mainLoop ()) 
-  { hIn := i, 
+runReader (mainLoop ())
+  { hIn := i,
     hOut := o,
     docRef := docRef,
     pendingRequestsRef := pendingRequestsRef
diff --git a/src/Lean/Server/Snapshots.lean b/src/Lean/Server/Snapshots.lean
index 8ec26255c7..77d4a58ddc 100644
--- a/src/Lean/Server/Snapshots.lean
+++ b/src/Lean/Server/Snapshots.lean
@@ -68,8 +68,7 @@ def compileHeader (contents : String) (opts : Options := {}) : IO Snapshot := do
 
 def reparseHeader (contents : String) (header : Snapshot) (opts : Options := {}) : IO Snapshot := do
 let inputCtx := Parser.mkInputContext contents "<input>";
-emptyEnv ← mkEmptyEnvironment;
-let (_, newHeaderParserState, _) := Parser.parseHeader emptyEnv inputCtx;
+(_, newHeaderParserState, _) ← Parser.parseHeader inputCtx;
 pure { header with mpState := newHeaderParserState }
 
 private def ioErrorFromEmpty (ex : Empty) : IO.Error :=
diff --git a/src/Lean/Server/Utils.lean b/src/Lean/Server/Utils.lean
index 5c62855aa2..9a990cd8b4 100644
--- a/src/Lean/Server/Utils.lean
+++ b/src/Lean/Server/Utils.lean
@@ -98,3 +98,14 @@ changes.foldr accumulateChanges (oldText, 0xffffffff)
 
 end Server
 end Lean
+
+namespace List
+
+universe u
+variable {α : Type u}
+
+def takeWhile (p : α → Bool) : List α → List α
+| []       => []
+| hd :: tl => if p hd then hd :: takeWhile tl else []
+
+end List
diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean
index c28fbde4c7..dd67c48b10 100644
--- a/src/Lean/Server/Watchdog.lean
+++ b/src/Lean/Server/Watchdog.lean
@@ -19,7 +19,7 @@ For general server architecture, see `README.md`. This module implements the wat
 
 ## Watchdog state
 
-Most LSP clients only send us file diffs, so to facilitate sending entire file contents to freshly restarted 
+Most LSP clients only send us file diffs, so to facilitate sending entire file contents to freshly restarted
 workers, the watchdog needs to maintain the current state of each file. It can also use this state to detect changes
 to the header and thus restart the corresponding worker, freeing its imports.
 
@@ -35,7 +35,7 @@ The watchdog process and its file worker processes communicate via LSP. If the n
 we might add non-standard commands similarly based on JSON-RPC. Most requests and notifications
 are forwarded to the corresponding file worker process, with the exception of these notifications:
 
-- textDocument/didOpen: Launch the file worker, create the associated watchdog state and launch a task to 
+- textDocument/didOpen: Launch the file worker, create the associated watchdog state and launch a task to
                         asynchronously receive LSP packets from the worker (e.g. request responses).
 - textDocument/didChange: Update the local file state. If the header was mutated,
                           signal a shutdown to the file worker by closing the I/O channels.
@@ -44,9 +44,9 @@ are forwarded to the corresponding file worker process, with the exception of th
 
 Moreover, we don't implement the full protocol at this level:
 
-- Upon starting, the `initialize` request is forwarded to the worker, but it must not respond with its server 
+- Upon starting, the `initialize` request is forwarded to the worker, but it must not respond with its server
   capabilities. Consequently, the watchdog will not send an `initialized` notification to the worker.
-- After `initialize`, the watchdog sends the corresponding `didOpen` notification with the full current state of 
+- After `initialize`, the watchdog sends the corresponding `didOpen` notification with the full current state of
   the file. No additional `didOpen` notifications will be forwarded to the worker process.
 - `$/cancelRequest` notifications are forwarded to all file workers.
 - File workers are always terminated with an `exit` notification, without previously receiving a `shutdown` request.
@@ -54,7 +54,7 @@ Moreover, we don't implement the full protocol at this level:
 
 ## Watchdog <-> client communication
 
-The watchdog itself should implement the LSP standard as closely as possible. However we reserve the right to add 
+The watchdog itself should implement the LSP standard as closely as possible. However we reserve the right to add
 non-standard extensions in case they're needed, for example to communicate tactic state.
 -/
 
@@ -72,9 +72,9 @@ structure OpenDocument :=
 (text : FileMap)
 (headerAst : Syntax)
 
-def workerCfg : Process.StdioConfig := 
-{ stdin  := Process.Stdio.piped, 
-  stdout := Process.Stdio.piped, 
+def workerCfg : Process.StdioConfig :=
+{ stdin  := Process.Stdio.piped,
+  stdout := Process.Stdio.piped,
   stderr := Process.Stdio.piped }
 
 -- Events that a forwarding task of a worker signals to the main task
@@ -83,12 +83,12 @@ inductive WorkerEvent
 | crashed (e : IO.Error)
 
 inductive WorkerState
--- The watchdog can detect a crashed file worker in two places: When trying to send a message to the file worker 
+-- The watchdog can detect a crashed file worker in two places: When trying to send a message to the file worker
 -- and when reading a request reply.
--- In the latter case, the forwarding task terminates and delegates a `crashed` event to the main task. 
+-- In the latter case, the forwarding task terminates and delegates a `crashed` event to the main task.
 -- Then, in both cases, the file worker has its state set to `crashed` and requests that are in-flight are errored.
--- Upon receiving the next packet for that file worker, the file worker is restarted and the packet is forwarded 
--- to it. If the crash was detected while writing a packet, we queue that packet until the next packet for the file 
+-- Upon receiving the next packet for that file worker, the file worker is restarted and the packet is forwarded
+-- to it. If the crash was detected while writing a packet, we queue that packet until the next packet for the file
 -- worker arrives.
 | crashed (queuedMsgs : Array JsonRpc.Message)
 | running
@@ -130,7 +130,7 @@ writeLspMessage fw.stdin msg
 def writeNotification {α : Type*} [HasToJson α] (fw : FileWorker) (method : String) (param : α) : m Unit :=
 writeLspNotification fw.stdin method param
 
-def writeRequest {α : Type*} [HasToJson α] (fw : FileWorker) (id : RequestID) (method : String) (param : α) 
+def writeRequest {α : Type*} [HasToJson α] (fw : FileWorker) (id : RequestID) (method : String) (param : α)
   : m Unit := do
 writeLspRequest fw.stdin id method param;
 liftIO $ fw.pendingRequestsRef.modify $ fun pendingRequests =>
@@ -187,7 +187,7 @@ partial def fwdMsgAux (fw : FileWorker) (hOut : FS.Stream) : Unit → IO WorkerE
         pure WorkerEvent.terminated
       else do
         -- worker crashed
-        fw.errorPendingRequests hOut ErrorCode.internalError 
+        fw.errorPendingRequests hOut ErrorCode.internalError
           "Server process of file crashed, likely due to a stack overflow in user code";
         pure (WorkerEvent.crashed err))
 
@@ -195,16 +195,15 @@ partial def fwdMsgAux (fw : FileWorker) (hOut : FS.Stream) : Unit → IO WorkerE
 which must be handled in the main watchdog thread (e.g. an I/O error) happens. -/
 def fwdMsgTask (fw : FileWorker) : ServerM (Task WorkerEvent) :=
 fun st =>
-  (Task.map (fun either => 
+  (Task.map (fun either =>
     match either with
     | Except.ok ev   => ev
-    | Except.error e => WorkerEvent.crashed e)) 
+    | Except.error e => WorkerEvent.crashed e))
   <$> (IO.asTask (fwdMsgAux fw st.hOut ()) Task.Priority.dedicated)
 
 private def parseHeaderAst (input : String) : IO Syntax := do
-emptyEnv ← mkEmptyEnvironment;
 let inputCtx    := Parser.mkInputContext input "<input>";
-let (stx, _, _) := Parser.parseHeader emptyEnv inputCtx;
+(stx, _, _) ← Parser.parseHeader inputCtx;
 pure stx
 
 def startFileWorker (uri : DocumentUri) (version : Nat) (text : FileMap) : ServerM Unit := do
@@ -213,7 +212,7 @@ headerAst ← monadLift $ parseHeaderAst text.source;
 workerProc ← monadLift $ Process.spawn { workerCfg with cmd := st.workerPath };
 pendingRequestsRef ← IO.mkRef (RBMap.empty : PendingRequestMap);
 -- the task will never access itself, so this is fine
-let commTaskFw : FileWorker := 
+let commTaskFw : FileWorker :=
   { doc                := ⟨version, text, headerAst⟩,
     proc               := workerProc,
     commTask           := Task.pure WorkerEvent.terminated,
@@ -222,12 +221,12 @@ let commTaskFw : FileWorker :=
 commTask ← fwdMsgTask commTaskFw;
 let fw : FileWorker := { commTaskFw with commTask := commTask };
 writeLspRequest fw.stdin (0 : Nat) "initialize" st.initParams;
-fw.writeNotification "textDocument/didOpen" 
-  { textDocument := 
-     { uri        := uri, 
-       languageId := "lean", 
-       version    := version, 
-       text       := text.source } 
+fw.writeNotification "textDocument/didOpen"
+  { textDocument :=
+     { uri        := uri,
+       languageId := "lean",
+       version    := version,
+       text       := text.source }
     : DidOpenTextDocumentParams };
 updateFileWorkers uri fw
 
@@ -251,7 +250,7 @@ def handleCrash (uri : DocumentUri) (queuedMsgs : Array JsonRpc.Message) : Serve
 fw ← findFileWorker uri;
 updateFileWorkers uri { fw with state := WorkerState.crashed queuedMsgs }
 
-def restartCrashedFileWorker (uri : DocumentUri) (fw : FileWorker) (queuedMsgs : Array JsonRpc.Message) 
+def restartCrashedFileWorker (uri : DocumentUri) (fw : FileWorker) (queuedMsgs : Array JsonRpc.Message)
   : ServerM Unit := do
 eraseFileWorker uri;
 startFileWorker uri fw.doc.version fw.doc.text;
@@ -308,7 +307,7 @@ terminateFileWorker p.textDocument.uri
 def handleCancelRequest (p : CancelParams) : ServerM Unit := do
 st ← read;
 fileWorkers ← st.fileWorkersRef.get;
-fileWorkers.forM $ fun uri fw => 
+fileWorkers.forM $ fun uri fw =>
   match fw.state with
   | WorkerState.crashed queuedMsgs => restartCrashedFileWorker uri fw queuedMsgs
   | WorkerState.running =>
@@ -354,7 +353,7 @@ inductive ServerEvent
 def runClientTask : ServerM (Task ServerEvent) := do
 st ← read;
 clientTask ← liftIO $ IO.asTask $ ServerEvent.ClientMsg <$> readLspMessage st.hIn;
-let clientTask := clientTask.map $ fun either => 
+let clientTask := clientTask.map $ fun either =>
   match either with
   | Except.ok ev   => ev
   | Except.error e => ServerEvent.ClientError e;
@@ -392,7 +391,7 @@ partial def mainLoop : Task ServerEvent → ServerM Unit
     | WorkerEvent.crashed e => do
       handleCrash uri #[];
       mainLoop clientTask
-    | WorkerEvent.terminated => throwServerError 
+    | WorkerEvent.terminated => throwServerError
       "Internal server error: got termination event for worker that should have been removed"
 
 def mkLeanServerCapabilities : ServerCapabilities :=
@@ -430,13 +429,13 @@ initRequest ← readLspRequestAs i "initialize" InitializeParams;
 writeLspResponse o initRequest.id
 { capabilities := mkLeanServerCapabilities,
   serverInfo?  := some { name     := "Lean 4 server",
-                         version? := "0.0.1" } 
+                         version? := "0.0.1" }
   : InitializeResult };
 runReader
   initAndRunWatchdogAux
   { hIn            := i,
     hOut           := o,
-    hLog           := e, 
+    hLog           := e,
     fileWorkersRef := fileWorkersRef,
     initParams     := initRequest.param,
     workerPath     := workerPath