From 89bbaf514e7faa0f4398b2c97eaa7837a714e26d Mon Sep 17 00:00:00 2001
From: larsk21 <57503246+larsk21@users.noreply.github.com>
Date: Fri, 7 Jan 2022 09:32:06 +0100
Subject: [PATCH] feat: include imports in header snap info tree

---
 src/Lean/Server/FileWorker.lean | 15 ++++++++++++---
 1 file changed, 12 insertions(+), 3 deletions(-)

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