From f4fc8ed57cd729016fc6f372e402c5a932ad4b44 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Wed, 26 Jul 2023 11:50:31 +0200 Subject: [PATCH] add optional argument checkForbiddenTactics to compileProof --- server/GameServer/FileWorker.lean | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/server/GameServer/FileWorker.lean b/server/GameServer/FileWorker.lean index c02b23d..1e38ef6 100644 --- a/server/GameServer/FileWorker.lean +++ b/server/GameServer/FileWorker.lean @@ -108,7 +108,8 @@ where addWarningMessage (info : SourceInfo) (s : MessageData) := open Elab Meta Expr in def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets : Bool) - (couldBeEndSnap : Bool) (levelParams : Game.DidOpenLevelParams) (initParams : Lsp.InitializeParams): IO Snapshot := do + (couldBeEndSnap : Bool) (levelParams : Game.DidOpenLevelParams) (initParams : Lsp.InitializeParams) + (checkForbiddenTactics := true) : IO Snapshot := do -- Recognize end snap if inputCtx.input.atEnd snap.mpState.pos ∧ couldBeEndSnap then let endSnap : Snapshot := { @@ -161,7 +162,8 @@ def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets parseResultRef.set (tacticStx, cmdParserState) -- Check for forbidden tactics - findForbiddenTactics inputCtx levelParams tacticStx + if checkForbiddenTactics then + findForbiddenTactics inputCtx levelParams tacticStx -- Insert invisible `skip` command to make sure we always display the initial goal let skip := Syntax.node (.original default 0 default endOfWhitespace) ``Lean.Parser.Tactic.skip #[]