From 8853b17fee59728700760eefbe1c1b8b079eb650 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 6 Mar 2024 15:14:08 -0800
Subject: [PATCH] test: More diagnostics for tests

---
 Pantograph/Goal.lean     | 4 ++++
 Pantograph/Protocol.lean | 2 +-
 Test/Integration.lean    | 6 ++++++
 3 files changed, 11 insertions(+), 1 deletion(-)

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 ({