From 8e35926b5cad34fa2b8e4747ad3056cdd896f686 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Tue, 24 Jun 2025 15:05:24 -0700
Subject: [PATCH] feat(goal): Tactic action site

---
 Pantograph/Goal.lean | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index a02e875..ec8facb 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -10,6 +10,27 @@ import Lean
 namespace Pantograph
 open Lean
 
+/-- Determine the acting area of a tactic -/
+inductive Site where
+  | focus (goal : MVarId)
+  | prefer (goal : MVarId)
+  | unfocus
+
+instance : Coe MVarId Site where
+  coe := .focus
+
+protected def Site.runTacticM (site : Site) { m } [Monad m] [MonadLiftT Elab.Tactic.TacticM m] [MonadControlT Elab.Tactic.TacticM m]
+  (f : m α) : m α :=
+  match site with
+  | .focus goal => do
+    Elab.Tactic.setGoals [goal]
+    f
+  | .prefer goal => do
+    let otherGoals := (← Elab.Tactic.getUnsolvedGoals).filter (· != goal)
+    Elab.Tactic.setGoals (goal :: otherGoals)
+    f
+  | .unfocus => f
+
 /--
 Represents an interconnected set of metavariables, or a state in proof search
  -/