Pantograph/Goal.lean

@@ -327,6 +327,16 @@ protected def GoalState.convExit (state: GoalState):
 
 
 
+protected def GoalState.focus (state: GoalState) (goalId: Nat): Option GoalState := do
+  let goal ← state.savedState.tactic.goals.get? goalId
+  return {
+    state with
+    savedState := {
+      state.savedState with
+      tactic := { goals := [goal] },
+    },
+  }
+
 /--
 Brings into scope a list of goals
 -/
@@ -345,7 +355,6 @@ protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except S
         tactic := { goals := unassigned },
       },
     }
-
 /--
 Brings into scope all goals from `branch`
 -/

Pantograph/Library.lean

@@ -178,14 +178,18 @@ def goalConv (state: GoalState) (goalId: Nat): Lean.CoreM TacticResult :=
 def goalConvExit (state: GoalState): Lean.CoreM TacticResult :=
   runTermElabM <| state.convExit
 
-@[export pantograph_goal_continue]
-def goalContinue (target: GoalState) (branch: GoalState): Except String GoalState :=
-  target.continue branch
+@[export pantograph_goal_focus]
+def goalFocus (state: GoalState) (goalId: Nat): Option GoalState :=
+  state.focus goalId
 
 @[export pantograph_goal_resume]
 def goalResume (target: GoalState) (goals: Array String): Except String GoalState :=
   target.resume (goals.map (λ n => { name := n.toName }) |>.toList)
 
+@[export pantograph_goal_continue]
+def goalContinue (target: GoalState) (branch: GoalState): Except String GoalState :=
+  target.continue branch
+
 @[export pantograph_goal_serialize_m]
 def goalSerialize (state: GoalState) (options: @&Protocol.Options): Lean.CoreM (Array Protocol.Goal) :=
   runMetaM <| state.serializeGoals (parent := .none) options