From 894d2708d859b4445295acfb61d09eea62f485f8 Mon Sep 17 00:00:00 2001
From: Alexander Bentkamp <bentkamp@gmail.com>
Date: Wed, 7 Dec 2022 18:24:26 +0100
Subject: [PATCH] add world parameter to router

---
 client/src/components/Level.tsx               |  5 +++--
 client/src/components/Welcome.tsx             |  2 +-
 client/src/index.tsx                          |  2 +-
 server/leanserver/GameServer/RpcHandlers.lean | 14 ++++++++------
 4 files changed, 13 insertions(+), 10 deletions(-)

diff --git a/client/src/components/Level.tsx b/client/src/components/Level.tsx
index 6179c3a..ef0bf85 100644
--- a/client/src/components/Level.tsx
+++ b/client/src/components/Level.tsx
@@ -31,6 +31,7 @@ function Level() {
 
   const params = useParams();
   const levelId = parseInt(params.levelId)
+  const worldId = params.worldId
 
   const [tacticDocs, setTacticDocs] = useState([])
   const [lemmaDocs, setLemmaDocs] = useState([])
@@ -105,7 +106,7 @@ function Level() {
     return () => { editor.dispose() }
   }, [])
 
-  const uri = `file:///level${levelId}`
+  const uri = `file:///${worldId}/${levelId}`
 
   // The next function will be called when the level changes
   useEffect(() => {
@@ -122,7 +123,7 @@ function Level() {
         new AbbreviationRewriter(new AbbreviationProvider(), model, editor)
 
 
-        leanClient.sendRequest("loadLevel", {world: "TestWorld", level: levelId}).then((res) => {
+        leanClient.sendRequest("loadLevel", {world: worldId, level: levelId}).then((res) => {
           // setLevelTitle("Level " + res["index"] + ": " + res["title"])
           // setIndex(parseInt(res["index"]))
           setTacticDocs(res["tactics"])
diff --git a/client/src/components/Welcome.tsx b/client/src/components/Welcome.tsx
index 8dadaf5..e2ee3d9 100644
--- a/client/src/components/Welcome.tsx
+++ b/client/src/components/Welcome.tsx
@@ -91,7 +91,7 @@ function Welcome() {
         </Typography>
       </Box>
       <Box textAlign='center' sx={{ m: 5 }}>
-        <Button component={RouterLink} to="/level/1" variant="contained">Start rescue mission</Button>
+        <Button component={RouterLink} to="/world/TestWorld/level/1" variant="contained">Start rescue mission</Button>
       </Box>
       <div ref={worldsRef} style={{"width": "100%","height": "50em"}} />
     </div>
diff --git a/client/src/index.tsx b/client/src/index.tsx
index 1c0799d..9c9790b 100644
--- a/client/src/index.tsx
+++ b/client/src/index.tsx
@@ -29,7 +29,7 @@ const router = createHashRouter([
         element: <Welcome />,
       },
       {
-        path: "/level/:levelId",
+        path: "/world/:worldId/level/:levelId",
         element: <Level />,
       },
     ],
diff --git a/server/leanserver/GameServer/RpcHandlers.lean b/server/leanserver/GameServer/RpcHandlers.lean
index 1f08a72..a231b0a 100644
--- a/server/leanserver/GameServer/RpcHandlers.lean
+++ b/server/leanserver/GameServer/RpcHandlers.lean
@@ -58,18 +58,20 @@ structure PlainGoal where
   goals : Array GameGoal
   deriving FromJson, ToJson
 
+#check String.split
+
 -- TODO: Find a better way to pass on the file name?
-def levelIdFromFileName [Monad m] [MonadError m] [MonadEnv m] (fileName : String) : m Nat := do
-  if fileName.startsWith "/level" then
-    if let some id := (fileName.drop "/level".length).toNat? then
-      return id
+def levelIdFromFileName [Monad m] [MonadError m] [MonadEnv m] (fileName : String) : m LevelId := do
+  let fileParts := fileName.splitOn "/"
+  if fileParts.length == 3 then
+    if let some level := fileParts[2]!.toNat? then
+      return {game := `TestGame, world := fileParts[1]!, level := level}
   throwError s!"Could not find level ID in file name: {fileName}"
-  return 1
 
 def getLevelByFileName [Monad m] [MonadError m] [MonadEnv m] (fileName : String) : m GameLevel := do
   let levelId ← levelIdFromFileName fileName
   -- TODO: make world and game configurable
-  let some level ← getLevel? {game := `TestGame, world := `TestWorld, level := levelId}
+  let some level ← getLevel? levelId
     | throwError "Level not found"
   return level