From 1f0d9aea4392a6634888edba261047d901738d8f Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Wed, 22 Feb 2023 15:10:46 +0100 Subject: [PATCH] check if tactic doc exists Fixes #34 --- server/leanserver/GameServer/Commands.lean | 17 ++++++++++++++--- 1 file changed, 14 insertions(+), 3 deletions(-) diff --git a/server/leanserver/GameServer/Commands.lean b/server/leanserver/GameServer/Commands.lean index 9068e41..f1b13c8 100644 --- a/server/leanserver/GameServer/Commands.lean +++ b/server/leanserver/GameServer/Commands.lean @@ -187,17 +187,28 @@ elab "TacticDoc" name:ident content:str : command => instance : Quote TacticDocEntry `term := ⟨λ entry => Syntax.mkCApp ``TacticDocEntry.mk #[quote entry.name, quote entry.content]⟩ +/-- Throw an error if tactic doc does not exist -/ +def checkTacticDoc (name : Name) : CommandElabM Unit := do + let some _ := (tacticDocExt.getState (← getEnv)).find? (·.name = name) + | throwError "Missing Tactic Documentation: {name}" + /-- Declare tactics that are introduced by this level. -/ elab "NewTactics" args:ident* : command => do - modifyCurLevel fun level => pure {level with newTactics := args.map (·.getId)} + let names := args.map (·.getId) + for name in names do checkTacticDoc name + modifyCurLevel fun level => pure {level with newTactics := names} /-- 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)} + let names := args.map (·.getId) + for name in names do checkTacticDoc name + modifyCurLevel fun level => pure {level with disabledTactics := names} /-- 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)} + let names := args.map (·.getId) + for name in names do checkTacticDoc name + modifyCurLevel fun level => pure {level with onlyTactics := names} /-! ## Lemmas -/