OnlyTactics command #16

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.

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) :=