Pantograph/Library.lean

@@ -138,16 +138,22 @@ def goalSerialize (state: GoalState) (options: @&Protocol.Options): CoreM (Array
   runMetaM <| state.serializeGoals (parent := .none) options
 
 @[export pantograph_goal_print_m]
-def goalPrint (state: GoalState) (options: @&Protocol.Options): CoreM Protocol.GoalPrintResult :=
+def goalPrint (state: GoalState) (extraMVars : Array String) (options: @&Protocol.Options): CoreM Protocol.GoalPrintResult :=
   runMetaM do
     state.restoreMetaM
     return {
-      root? := ← state.rootExpr?.mapM (λ expr =>
+      root? := ← state.rootExpr?.mapM λ expr =>
         state.withRootContext do
-          serializeExpression options (← instantiateAll expr)),
+          serializeExpression options (← instantiateAll expr),
-      parent? := ← state.parentExpr?.mapM (λ expr =>
+      parent? := ← state.parentExpr?.mapM λ expr =>
         state.withParentContext do
-          serializeExpression options (← instantiateAll expr)),
+          serializeExpression options (← instantiateAll expr),
+      extraMVars := ← extraMVars.mapM λ mvarId => do
+        let mvarId: MVarId := { name := mvarId.toName }
+        let .some _ ← mvarId.findDecl? | return {}
+        state.withContext mvarId do
+          let .some expr ← getExprMVarAssignment? mvarId | return {}
+          serializeExpression options (← instantiateAll expr),
     }
 
 @[export pantograph_goal_tactic_m]

Pantograph/Protocol.lean

@@ -271,12 +271,16 @@ structure GoalDeleteResult where
 
 structure GoalPrint where
   stateId: Nat
+  -- Print values of extra mvars
+  extraMVars?: Option (Array String) := .none
   deriving Lean.FromJson
 structure GoalPrintResult where
   -- The root expression
   root?: Option Expression := .none
   -- The filling expression of the parent goal
   parent?: Option Expression
+
+  extraMVars: Array Expression := #[]
   deriving Lean.ToJson
 
 -- Diagnostic Options, not available in REPL

Repl.lean

@@ -222,7 +222,8 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     let state ← get
     let .some goalState := state.goalStates[args.stateId]? |
       return .error $ errorIndex s!"Invalid state index {args.stateId}"
-    let result ← runMetaInMainM <| goalPrint goalState state.options
+    let extraMVars := args.extraMVars?.getD #[]
+    let result ← runMetaInMainM <| goalPrint goalState extraMVars state.options
     return .ok result
   goal_save (args: Protocol.GoalSave): MainM (CR Protocol.GoalSaveResult) := do
     let state ← get