From 0273d6a46526afcc96ba4fad9100ed3e9145e396 Mon Sep 17 00:00:00 2001
From: Alexander Bentkamp <bentkamp@gmail.com>
Date: Wed, 30 Nov 2022 17:28:11 +0100
Subject: [PATCH] fix server error due to missing info tree in header snap

---
 server/leanserver/GameServer/FileWorker.lean | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/server/leanserver/GameServer/FileWorker.lean b/server/leanserver/GameServer/FileWorker.lean
index f9466dd..127e928 100644
--- a/server/leanserver/GameServer/FileWorker.lean
+++ b/server/leanserver/GameServer/FileWorker.lean
@@ -293,6 +293,17 @@ section Initialization
         headerEnv := headerEnv.setMainModule (← moduleNameOfFileName path none)
     catch _ => pure ()
     let cmdState := Elab.Command.mkState headerEnv {} opts
+    let cmdState := { cmdState with infoState := {
+      enabled := true
+      trees := #[Elab.InfoTree.context ({
+        env     := headerEnv
+        fileMap := m.text
+        ngen    := { namePrefix := `_worker }
+      }) (Elab.InfoTree.node
+          (Elab.Info.ofCommandInfo { elaborator := `header, stx := Syntax.missing })
+          #[].toPArray'
+      )].toPArray'
+    }}
     let headerSnap := {
       beginPos := 0
       stx := Syntax.missing