From 6e046d72b66d841f9d0e5f9422ea6b04b4c187ea Mon Sep 17 00:00:00 2001
From: Jon <jon.eugster@gmx.ch>
Date: Sat, 7 Oct 2023 21:03:44 +0200
Subject: [PATCH] show error on duplicated level number

---
 server/GameServer/EnvExtensions.lean | 9 +++++++--
 server/test/test_statement.lean      | 5 ++++-
 2 files changed, 11 insertions(+), 3 deletions(-)

diff --git a/server/GameServer/EnvExtensions.lean b/server/GameServer/EnvExtensions.lean
index 400c4f5..5d0a92d 100644
--- a/server/GameServer/EnvExtensions.lean
+++ b/server/GameServer/EnvExtensions.lean
@@ -382,8 +382,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
-    return {world with levels := world.levels.insert level.index level}
+  let worldId ← getCurWorldId
+  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)
diff --git a/server/test/test_statement.lean b/server/test/test_statement.lean
index e8cbe9b..eb2f79c 100644
--- a/server/test/test_statement.lean
+++ b/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