diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean
index b0e2b86aac..301ed343c1 100644
--- a/src/Lean/Server/FileWorker.lean
+++ b/src/Lean/Server/FileWorker.lean
@@ -217,9 +217,18 @@ section Initialization
     let cmdState := Elab.Command.mkState headerEnv msgLog opts
     let cmdState := { cmdState with infoState := {
       enabled := true
-      -- add dummy tree for invariant in `Snapshot.infoTree`
-      -- TODO: maybe even fill with useful stuff
-      trees := #[Elab.InfoTree.node (Elab.Info.ofCommandInfo { elaborator := `import, stx := headerStx }) #[].toPersistentArray].toPersistentArray
+      trees := #[Elab.InfoTree.context ({
+        env := headerEnv
+        fileMap := m.text
+      }) (Elab.InfoTree.node
+          (Elab.Info.ofCommandInfo { elaborator := `import, stx := headerStx })
+          (headerStx[1].getArgs.toList.map (fun importStx =>
+            Elab.InfoTree.node (Elab.Info.ofCommandInfo {
+              elaborator := Name.anonymous,
+              stx := importStx
+            }) #[].toPersistentArray
+          )).toPersistentArray
+      )].toPersistentArray
     }}
     let headerSnap := {
       beginPos := 0