diff --git a/src/Lean/Data/Lsp/Extra.lean b/src/Lean/Data/Lsp/Extra.lean
index 33f36f1558..1c48490214 100644
--- a/src/Lean/Data/Lsp/Extra.lean
+++ b/src/Lean/Data/Lsp/Extra.lean
@@ -18,7 +18,7 @@ structure LeanDidOpenTextDocumentParams extends DidOpenTextDocumentParams where
   /--
     Further flags passed to `lake print-paths` for the opened document.
     Used for forwarding `--no-build` on initial open. -/
-  extraPrintPathsFlags? : Option (Array String)
+  extraPrintPathsFlags? : Option (Array String) := none
   deriving FromJson, ToJson
 
 /-- `textDocument/waitForDiagnostics` client->server request.
diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean
index 1657b9506c..1c9bd3b7c1 100644
--- a/src/Lean/Server/FileWorker.lean
+++ b/src/Lean/Server/FileWorker.lean
@@ -159,7 +159,7 @@ section Initialization
   Compilation progress is reported to `hOut` via LSP notifications. Return the search path for
   source files. -/
   partial def lakeSetupSearchPath (lakePath : System.FilePath) (m : DocumentMeta) (imports : Array Import) (hOut : FS.Stream) : IO SearchPath := do
-    let args := #["print-paths"] ++ imports.map (toString ·.module)
+    let args := #["print-paths"] ++ imports.map (toString ·.module) ++ m.extraPrintPathsFlags
     let cmdStr := " ".intercalate (toString lakePath :: args.toList)
     let lakeProc ← Process.spawn {
       stdin  := Process.Stdio.null
@@ -336,7 +336,7 @@ section NotificationHandling
     let newVersion := docId.version?.getD 0
     if ¬ changes.isEmpty then
       let newDocText := foldDocumentChanges changes oldDoc.meta.text
-      updateDocument ⟨docId.uri, newVersion, newDocText⟩
+      updateDocument ⟨docId.uri, newVersion, newDocText, oldDoc.meta.extraPrintPathsFlags⟩
 
   def handleCancelRequest (p : CancelParams) : WorkerM Unit := do
     updatePendingRequests (fun pendingRequests => pendingRequests.erase p.id)
@@ -476,14 +476,15 @@ def initAndRunWorker (i o e : FS.Stream) (opts : Options) : IO UInt32 := do
   let i ← maybeTee "fwIn.txt" false i
   let o ← maybeTee "fwOut.txt" true o
   let initParams ← i.readLspRequestAs "initialize" InitializeParams
-  let ⟨_, param⟩ ← i.readLspNotificationAs "textDocument/didOpen" DidOpenTextDocumentParams
+  let ⟨_, param⟩ ← i.readLspNotificationAs "textDocument/didOpen" LeanDidOpenTextDocumentParams
+  let extraPrintPathsFlags := param.extraPrintPathsFlags?.getD #[]
   let doc := param.textDocument
   /- NOTE(WN): `toFileMap` marks line beginnings as immediately following
     "\n", which should be enough to handle both LF and CRLF correctly.
     This is because LSP always refers to characters by (line, column),
     so if we get the line number correct it shouldn't matter that there
     is a CR there. -/
-  let meta : DocumentMeta := ⟨doc.uri, doc.version, doc.text.toFileMap⟩
+  let meta : DocumentMeta := ⟨doc.uri, doc.version, doc.text.toFileMap, extraPrintPathsFlags⟩
   let e := e.withPrefix s!"[{param.textDocument.uri}] "
   let _ ← IO.setStderr e
   try
diff --git a/src/Lean/Server/Utils.lean b/src/Lean/Server/Utils.lean
index 4827739d42..ee0fd9cc9c 100644
--- a/src/Lean/Server/Utils.lean
+++ b/src/Lean/Server/Utils.lean
@@ -65,9 +65,10 @@ end IO
 namespace Lean.Server
 
 structure DocumentMeta where
-  uri     : Lsp.DocumentUri
-  version : Nat
-  text    : FileMap
+  uri                  : Lsp.DocumentUri
+  version              : Nat
+  text                 : FileMap
+  extraPrintPathsFlags : Array String
   deriving Inhabited
 
 def DocumentMeta.mkInputContext (doc : DocumentMeta) : Parser.InputContext where
diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean
index ee03f9a454..278d6ea177 100644
--- a/src/Lean/Server/Watchdog.lean
+++ b/src/Lean/Server/Watchdog.lean
@@ -237,7 +237,7 @@ section ServerM
       | Except.ok ev   => ev
       | Except.error e => WorkerEvent.ioError e
 
-  def startFileWorker (m : DocumentMeta) (extraPrintPathsFlags : Array String := #[]) : ServerM Unit := do
+  def startFileWorker (m : DocumentMeta) : ServerM Unit := do
     publishProgressAtPos m 0 (← read).hOut
     let st ← read
     let workerProc ← Process.spawn {
@@ -268,7 +268,7 @@ section ServerM
           version    := m.version
           text       := m.text.source
         }
-        extraPrintPathsFlags? := extraPrintPathsFlags
+        extraPrintPathsFlags? := m.extraPrintPathsFlags
         : LeanDidOpenTextDocumentParams
       }
     }
@@ -388,7 +388,7 @@ section NotificationHandling
        This is because LSP always refers to characters by (line, column),
        so if we get the line number correct it shouldn't matter that there
        is a CR there. -/
-    startFileWorker ⟨doc.uri, doc.version, doc.text.toFileMap⟩ (p.extraPrintPathsFlags?.getD #[])
+    startFileWorker ⟨doc.uri, doc.version, doc.text.toFileMap, p.extraPrintPathsFlags?.getD #[]⟩
 
   def handleDidChange (p : DidChangeTextDocumentParams) : ServerM Unit := do
     let doc := p.textDocument
@@ -399,7 +399,7 @@ section NotificationHandling
     if changes.isEmpty then
       return
     let newDocText := foldDocumentChanges changes oldDoc.text
-    let newDoc : DocumentMeta := ⟨doc.uri, newVersion, newDocText⟩
+    let newDoc : DocumentMeta := ⟨doc.uri, newVersion, newDocText, oldDoc.extraPrintPathsFlags⟩
     updateFileWorkers { fw with doc := newDoc }
     tryWriteMessage doc.uri (Notification.mk "textDocument/didChange" p) (restartCrashedWorker := true)