fix allowed keywords that are not tactics

server/GameServer/EnvExtensions.lean

@@ -4,6 +4,11 @@ import GameServer.Hints
 
 open GameServer
 
+-- TODO: Is there a better place?
+/-- Keywords that the server should not consider as tactics. -/
+def GameServer.ALLOWED_KEYWORDS : List String :=
+  ["with", "fun", "at", "only", "by", "generalizing"]
+
 /-- The default game name if `Game "MyGame"` is not used. -/
 def defaultGameName: String := "MyGame"
 -- Note: When changing any of these default names, one also needs to change them in `index.mjs`

server/GameServer/FileWorker.lean

@@ -122,7 +122,7 @@ partial def findForbiddenTactics (inputCtx : Parser.InputContext) (workerState :
     -- Atoms might be tactic names or other keywords.
     -- Note: We whitelisted known keywords because we cannot
     -- distinguish keywords from tactic names.
-    let allowed := ["with", "fun", "at", "only", "by", "to", "generalizing", "says"]
+    let allowed := GameServer.ALLOWED_KEYWORDS
     -- Ignore syntax elements that do not start with a letter or are listed above.
     if 0 < val.length ∧ val.data[0]!.isAlpha ∧ not (allowed.contains val) then
       -- Treat `simp?` and `simp!` like `simp`

server/GameServer/Inventory.lean

@@ -121,7 +121,7 @@ partial def collectUsedInventory (stx : Syntax) (acc : UsedInventory := {}) : Co
   | .atom _info val =>
     -- ignore syntax elements that do not start with a letter
     -- and ignore some standard keywords
-    let allowed := ["with", "fun", "at", "only", "by"]
+    let allowed := GameServer.ALLOWED_KEYWORDS
     if 0 < val.length ∧ val.data[0]!.isAlpha ∧ not (allowed.contains val) then
       let val := val.dropRightWhile (fun c => c == '!' || c == '?') -- treat `simp?` and `simp!` like `simp`
       return {acc with tactics := acc.tactics.insert val}