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() {
-
+
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: ,
},
{
- path: "/level/:levelId",
+ path: "/world/:worldId/level/:levelId",
element: ,
},
],
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