Merge pull request #116 from leanprover-community/eugster/level-error-msg

fix: show error on duplicated level number

server/GameServer/EnvExtensions.lean

@@ -386,8 +386,13 @@ def modifyCurWorld (fn : World → m World) [MonadError m] : m Unit := do
     return {game with worlds := {game.worlds with nodes := game.worlds.nodes.insert world.name (← fn world) }}
 
 def addLevel (level : GameLevel) [MonadError m] : m Unit := do
-  modifyCurWorld fun world => do
+  let worldId ← getCurWorldId
-    return {world with levels := world.levels.insert level.index level}
+  match ← getLevel? ⟨← getCurGameId, worldId, level.index⟩ with
+  | some _existingLevel =>
+    throwError m!"Level {level.index} already exists for world {worldId}!"
+  | none =>
+    modifyCurWorld fun world => do
+      return {world with levels := world.levels.insert level.index level}
 
 def getCurLevel [MonadError m] : m GameLevel := do
   let some level := (← getCurWorld).levels.find? (← getCurLevelIdx)

server/test/test_statement.lean

@@ -13,8 +13,11 @@ Level 1
 Statement foo.bar : 5 ≤ 7 := by
   simp
 
--- Shows warning on `foo.bar₂`:
+Game "Test"
+World "TestW"
+Level 2 -- should warn if set to `1`
 
+-- Shows warning on `foo.bar₂`:
 Statement foo.bar2 : 3 ≤ 7 := by
   simp