From cd27b2026c543289ce39439e26bb638862282357 Mon Sep 17 00:00:00 2001
From: Alexander Bentkamp <bentkamp@gmail.com>
Date: Mon, 6 Feb 2023 15:31:26 +0100
Subject: [PATCH] OnlyTactics command #16

---
 server/leanserver/GameServer/Commands.lean   | 9 ++++++---
 server/leanserver/GameServer/FileWorker.lean | 3 ++-
 2 files changed, 8 insertions(+), 4 deletions(-)

diff --git a/server/leanserver/GameServer/Commands.lean b/server/leanserver/GameServer/Commands.lean
index 38bae1e..231a9a9 100644
--- a/server/leanserver/GameServer/Commands.lean
+++ b/server/leanserver/GameServer/Commands.lean
@@ -187,15 +187,18 @@ elab "TacticDoc" name:ident content:str : command =>
 instance : Quote TacticDocEntry `term :=
 ⟨λ entry => Syntax.mkCApp ``TacticDocEntry.mk #[quote entry.name, quote entry.content]⟩
 
-/-- Declare the list of tactics that will be displayed in the current level.
-Expects a space separated list of identifiers that refer to either a tactic doc
-entry or a tactic doc set. -/
+/-- Declare tactics that are introduced by this level. -/
 elab "NewTactics" args:ident* : command => do
   modifyCurLevel fun level => pure {level with newTactics := args.map (·.getId)}
 
+/-- Declare tactics that are temporarily disabled in this level -/
 elab "DisabledTactics" args:ident* : command => do
   modifyCurLevel fun level => pure {level with disabledTactics := args.map (·.getId)}
 
+/-- Temporarily disable all tactics except the ones declared here -/
+elab "OnlyTactics" args:ident* : command => do
+  modifyCurLevel fun level => pure {level with onlyTactics := args.map (·.getId)}
+
 /-! ## Lemmas -/
 
 /-- Declare a documentation entry for some lemma.
diff --git a/server/leanserver/GameServer/FileWorker.lean b/server/leanserver/GameServer/FileWorker.lean
index b0dc577..88c7d61 100644
--- a/server/leanserver/GameServer/FileWorker.lean
+++ b/server/leanserver/GameServer/FileWorker.lean
@@ -79,7 +79,8 @@ partial def findForbiddenTactics (inputCtx : Parser.InputContext) (level : GameL
     if 0 < val.length ∧ val.data[0]!.isAlpha then
       if ¬ ((level.tactics.map (·.name.toString))).contains val then
         addErrorMessage info s!"You have not unlocked the tactic '{val}' yet!"
-      else if level.disabledTactics.contains val then
+      else if level.disabledTactics.contains val
+        ∨ (¬ level.onlyTactics.isEmpty ∧ ¬ level.onlyTactics.contains val)then
         addErrorMessage info s!"The tactic '{val}' is disabled in this level!"
   | .ident info rawVal val preresolved => return ()
 where addErrorMessage (info : SourceInfo) (s : MessageData) :=