From 50ec616b8e5df83472d0faf3047101eb6dbfd5c5 Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Mon, 28 Aug 2023 11:33:01 +0200
Subject: [PATCH] automate lemmaTab #88

---
 server/GameServer/Game.lean | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/server/GameServer/Game.lean b/server/GameServer/Game.lean
index 90d68cf..6895c48 100644
--- a/server/GameServer/Game.lean
+++ b/server/GameServer/Game.lean
@@ -153,7 +153,13 @@ partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do
             descrFormat := lvl.descrFormat --toExpr <| format (lvl.goal.raw) --toString <| Syntax.formatStx (lvl.goal.raw) --Syntax.formatStx (lvl.goal.raw) , -- TODO
             introduction := lvl.introduction
             conclusion := lvl.conclusion
-            lemmaTab := lvl.lemmaTab
+            lemmaTab := match lvl.lemmaTab with
+            | some tab => tab
+            | none =>
+              -- Try to set the lemma tab to the category of the first added lemma
+              match lvl.lemmas.tiles.find? (·.new) with
+              | some tile => tile.category
+              | none => none
             statementName := match lvl.statementName with
               | .anonymous => none
               | name => match (inventoryExt.getState env).find?