read level module form json

server/GameServer/EnvExtensions.lean

@@ -293,6 +293,7 @@ structure LevelInfo where
   descrText : Option String := none
   descrFormat : String := ""
   lemmaTab : Option String
+  module : Name
   displayName : Option String
   statementName : Option String
   template : Option String
@@ -317,6 +318,7 @@ def GameLevel.toInfo (lvl : GameLevel) (env : Environment) : LevelInfo :=
       | some tile => tile.category
       | none => none
     statementName := lvl.statementName.toString
+    module := lvl.module
     displayName := match lvl.statementName with
       | .anonymous => none
       | name => match (inventoryExt.getState env).find?

server/GameServer/FileWorker.lean

@@ -57,14 +57,7 @@ open IO
 open Snapshots
 open JsonRpc
 
--- TODO: check what's necessary and what is constant:
 structure GameWorkerState :=
-  -- uri : String
-  -- gameDir : String
-  -- levelModule : Name
-  -- tactics : Array InventoryTile
-  -- lemmas : Array InventoryTile
-  -- definitions : Array InventoryTile
   inventory : Array String
   /--
   Check for tactics/theorems that are not unlocked.
@@ -415,7 +408,7 @@ section Initialization
     fileMap  := default
 
   def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWidgets : Bool)
-      (gameDir : String) :
+      (gameDir : String) (module : Name):
       IO (Syntax × Task (Except Error (Snapshot × SearchPath))) := do
     -- Determine search paths of the game project by running `lake env printenv LEAN_PATH`.
     let out ← IO.Process.output
@@ -431,10 +424,7 @@ section Initialization
     -- Set the search path
     Lean.searchPathRef.set paths
 
-    --TODO:
-    let levelModule := `Game
-    let env ← importModules' #[{ module := `Init : Import }, { module := levelModule : Import }]
-    -- return (env, paths)
+    let env ← importModules' #[{ module := `Init : Import }, { module := module : Import }]
 
     -- use empty header
     let (headerStx, headerParserState, msgLog) ← Parser.parseHeader
@@ -483,8 +473,11 @@ section Initialization
     let rootUri? : Option String := some (toString game.name)
     let initParams := {initParams with rootUri?}
     let clientHasWidgets := initParams.initializationOptions?.bind (·.hasWidgets?) |>.getD false
+    let some (levelId : LevelId) := GameServer.levelIdFromFileName? initParams meta.mkInputContext.fileName
+      | throwServerError "Could not determine level ID"
+    let level ← loadLevelData gameDir levelId.world levelId.level
     let (headerStx, headerTask) ← compileHeader meta o opts (hasWidgets := clientHasWidgets)
-      gameDir
+      gameDir level.module
     let cancelTk ← CancelToken.new
     let ctx :=
       { hIn  := i

server/GameServer/SaveData.lean

@@ -59,10 +59,10 @@ def saveGameData (allItemsByType : HashMap InventoryType (HashSet Name))
 
   IO.FS.writeFile (path / inventoryFileName) (toString (toJson inventory))
 
-open GameData in
-def loadGameData (gameDir : System.FilePath) : IO Game := do
-  let path := gameDir / gameDataPath
-  let str ← IO.FS.readFile (path / gameFileName)
+open GameData
+
+def loadData (f : System.FilePath) (α : Type) [FromJson α] : IO α := do
+  let str ← IO.FS.readFile f
   let json ← match Json.parse str with
   | .ok v => pure v
   | .error e => throw (IO.userError e)
@@ -70,3 +70,9 @@ def loadGameData (gameDir : System.FilePath) : IO Game := do
   | .ok v => pure v
   | .error e => throw (IO.userError e)
   return data
+
+def loadGameData (gameDir : System.FilePath) : IO Game :=
+  loadData (gameDir / gameDataPath / gameFileName) Game
+
+def loadLevelData (gameDir : System.FilePath) (worldId : Name) (levelId : Nat) : IO LevelInfo :=
+  loadData (gameDir / gameDataPath / levelFileName worldId levelId) LevelInfo