From af8463ca5d09397848ad0d25e058af6752a1eb5f Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Wed, 14 Feb 2024 16:22:10 +0100
Subject: [PATCH] fixes for v4.6.0-rc1

---
 server/GameServer/FileWorker.lean      | 12 +++++++++---
 server/GameServer/InteractiveGoal.lean |  2 +-
 2 files changed, 10 insertions(+), 4 deletions(-)

diff --git a/server/GameServer/FileWorker.lean b/server/GameServer/FileWorker.lean
index 2d4f6b1..6740ffb 100644
--- a/server/GameServer/FileWorker.lean
+++ b/server/GameServer/FileWorker.lean
@@ -304,7 +304,7 @@ where
   private def publishIleanInfo (method : String) (m : DocumentMeta) (hOut : FS.Stream)
       (snaps : Array Snapshot) : IO Unit := do
     let trees := snaps.map fun snap => snap.infoTree
-    let references := findModuleRefs m.text trees (localVars := true)
+    let references ← findModuleRefs m.text trees (localVars := true) |>.toLspModuleRefs
     let param := { version := m.version, references : LeanIleanInfoParams }
     hOut.writeLspNotification { method, param }
 
@@ -508,6 +508,12 @@ def DocumentMeta.mkInputContext (doc : DocumentMeta) : Parser.InputContext where
   fileName := (System.Uri.fileUriToPath? doc.uri).getD doc.uri |>.toString
   fileMap  := default
 
+/-- `gameDir` and `module` were added.
+
+TODO: In general this resembles little similarity with the
+original code, and I don't know why...
+-/
+-- @[inherit_doc Lean.Server.FileWorker.compileHeader]
 def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWidgets : Bool)
     (gameDir : String) (module : Name):
     IO (Syntax × Task (Except Error (Snapshot × SearchPath))) := do
@@ -543,7 +549,7 @@ def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWid
     let cmdState := Elab.Command.mkState headerEnv {} opts
     let cmdState := { cmdState with infoState := {
       enabled := true
-      trees := #[Elab.InfoTree.context ({
+      trees := #[Elab.InfoTree.context (.commandCtx {
         env     := headerEnv
         fileMap := m.text
         ngen    := { namePrefix := `_worker }
@@ -560,7 +566,7 @@ def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWid
     let headerSnap := {
       beginPos := 0
       stx := headerStx
-      mpState := {}
+      mpState := {} -- was `headerParserState`
       cmdState := cmdState
       interactiveDiags := ← cmdState.messages.msgs.mapM (Widget.msgToInteractiveDiagnostic m.text · hasWidgets)
       tacticCache := (← IO.mkRef {})
diff --git a/server/GameServer/InteractiveGoal.lean b/server/GameServer/InteractiveGoal.lean
index 0377f24..f9b754b 100644
--- a/server/GameServer/InteractiveGoal.lean
+++ b/server/GameServer/InteractiveGoal.lean
@@ -146,7 +146,7 @@ def goalToInteractive (mvarId : MVarId) : MetaM InteractiveGoal := do
     return {
       hyps
       type := goalFmt
-      ctx := ⟨← Elab.ContextInfo.save⟩
+      ctx := ⟨{← Elab.CommandContextInfo.save with }⟩
       userName?
       goalPrefix := getGoalPrefix mvarDecl
       mvarId