From 9a04fd48196951000874a545f287e90febd7a2a3 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 8 Apr 2024 13:12:51 -0700
Subject: [PATCH] feat: Focus command

---
 Pantograph/Goal.lean    | 11 ++++++++++-
 Pantograph/Library.lean | 10 +++++++---
 2 files changed, 17 insertions(+), 4 deletions(-)

diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index 07a432b..7609dae 100644
--- a/Pantograph/Goal.lean
+++ b/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`
 -/
diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean
index 6da555d..0febba4 100644
--- a/Pantograph/Library.lean
+++ b/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