From b64adf31cfa319bd220fb821ee6521c56d00b171 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Thu, 14 Mar 2024 16:34:01 -0700
Subject: [PATCH] feat(lib): Export goal.print function

---
 Pantograph.lean         | 8 +-------
 Pantograph/Library.lean | 9 +++++++++
 2 files changed, 10 insertions(+), 7 deletions(-)

diff --git a/Pantograph.lean b/Pantograph.lean
index fceac00..bcf8395 100644
--- a/Pantograph.lean
+++ b/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
diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean
index d72fd3a..52a88b6 100644
--- a/Pantograph/Library.lean
+++ b/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