Pantograph.lean

@@ -179,12 +179,6 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     match state.goalStates.find? args.stateId with
     | .none => return .error $ errorIndex s!"Invalid state index {args.stateId}"
     | .some goalState => runMetaM <| do
-      goalState.restoreMetaM
-      let root? ← goalState.rootExpr?.mapM (λ expr => serialize_expression state.options expr)
-      let parent? ← goalState.parentExpr?.mapM (λ expr => serialize_expression state.options expr)
-      return .ok {
-        root?,
-        parent?,
-      }
+      return .ok (← goalPrint goalState state.options)
 
 end Pantograph

Pantograph/Library.lean

@@ -165,6 +165,15 @@ def goalResume (target: GoalState) (goals: Array String): Except String GoalStat
 def goalSerialize (state: GoalState) (options: @&Protocol.Options): Lean.CoreM (Array Protocol.Goal) :=
   runMetaM <| state.serializeGoals (parent := .none) options
 
+@[export pantograph_goal_print_m]
+def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Protocol.GoalPrintResult := do
+  let metaM := do
+    state.restoreMetaM
+    return {
+      root? := ← state.rootExpr?.mapM (λ expr => serialize_expression options expr),
+      parent? := ← state.parentExpr?.mapM (λ expr => serialize_expression options expr),
+    }
+  runMetaM metaM
 
 
 end Pantograph