From a90d3a59be6ee411c55fbda6e19ff3f4b6e7ac5e Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Thu, 17 Mar 2022 13:47:59 -0700 Subject: [PATCH] feat: lightweight support for optional pp in raw tactic state --- Mathport/Syntax/Parse.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Mathport/Syntax/Parse.lean b/Mathport/Syntax/Parse.lean index 59193fd87..f1eb46958 100644 --- a/Mathport/Syntax/Parse.lean +++ b/Mathport/Syntax/Parse.lean @@ -891,6 +891,7 @@ instance : FromJson RawGoal where structure RawTacticState where decl : Name goals : Array RawGoal + pp : Option String -- Note: we do not propagate this to AST3.TacticState deriving FromJson deriving instance FromJson for AST3.Comment @@ -1015,7 +1016,7 @@ def RawGoal.build : RawGoal → AST3.Goal | ⟨hyps, target⟩ => ⟨hyps.map (·.build exprs), exprs[target]⟩ def RawTacticState.build : RawTacticState → Name × Array AST3.Goal - | ⟨declName, goals⟩ => (declName, goals.map (·.build exprs)) + | ⟨declName, goals, _⟩ => (declName, goals.map (·.build exprs)) def RawTacticInvocation.build (states : Array (Name × Array AST3.Goal))