diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 630637d..b56c893 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -225,6 +225,10 @@ protected def GoalState.parentExpr? (goalState: GoalState): Option Expr := do let expr := goalState.mctx.eAssignment.find! parent let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr) return expr +protected def GoalState.assignedExprOf? (goalState: GoalState) (mvar: MVarId): Option Expr := do + let expr ← goalState.mctx.eAssignment.find? mvar + let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr) + return expr end Pantograph diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index 84e0cc2..a4983d9 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -242,7 +242,7 @@ structure GoalPrintResult where -- The root expression root?: Option Expression := .none -- The filling expression of the parent goal - parent?: Option Expression := .none + parent?: Option Expression deriving Lean.ToJson -- Diagnostic Options, not available in REPL diff --git a/Test/Integration.lean b/Test/Integration.lean index 0a6c210..8f3f217 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -103,6 +103,12 @@ def test_tactic : IO LSpec.TestSeq := goals? := #[goal1], }: Protocol.GoalTacticResult)), + subroutine_step "goal.print" + [("stateId", .num 1)] + (Lean.toJson ({ + parent? := .some { pp? := .some "fun x => ?m.11 x" }, + }: + Protocol.GoalPrintResult)), subroutine_step "goal.tactic" [("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "intro y")] (Lean.toJson ({