Pantograph/Goal.lean

@@ -225,10 +225,6 @@ 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

Pantograph/Protocol.lean

@@ -243,7 +243,7 @@ structure GoalPrintResult where
   -- The root expression
   root?: Option Expression := .none
   -- The filling expression of the parent goal
-  parent?: Option Expression
+  parent?: Option Expression := .none
   deriving Lean.ToJson
 
 -- Diagnostic Options, not available in REPL

Test/Integration.lean

@@ -97,12 +97,6 @@ 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 ({