From 4d9e2297079e9624edb0217fd0c1b5e4924883d0 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Thu, 26 Jun 2025 12:11:27 -0700
Subject: [PATCH] refactor(repl): Tactic into goal section

---
 Repl.lean | 24 ++++++++++++++----------
 1 file changed, 14 insertions(+), 10 deletions(-)

diff --git a/Repl.lean b/Repl.lean
index 9927d6e..54d1bb6 100644
--- a/Repl.lean
+++ b/Repl.lean
@@ -97,16 +97,7 @@ def liftTermElabM { α } (termElabM : Elab.TermElabM α) (levelNames : List Name
   }
   runCoreM $ termElabM.run' context state |>.run'
 
-section Frontend
-
-structure CompilationUnit where
-  -- Environment immediately before the unit
-  env : Environment
-  boundary : Nat × Nat
-  invocations : List Protocol.InvokedTactic
-  sorrys : List Frontend.InfoWithContext
-  messages : Array String
-  newConstants : List Name
+section Goal
 
 def goal_tactic (args: Protocol.GoalTactic): EMainM Protocol.GoalTacticResult := do
   let state ← getMainState
@@ -175,6 +166,19 @@ def goal_tactic (args: Protocol.GoalTactic): EMainM Protocol.GoalTacticResult :=
   | .ok (.failure messages) =>
     return { messages? := .some messages }
 
+end Goal
+
+section Frontend
+
+structure CompilationUnit where
+  -- Environment immediately before the unit
+  env : Environment
+  boundary : Nat × Nat
+  invocations : List Protocol.InvokedTactic
+  sorrys : List Frontend.InfoWithContext
+  messages : Array String
+  newConstants : List Name
+
 def frontend_process (args: Protocol.FrontendProcess): EMainM Protocol.FrontendProcessResult := do
   let options := (← getMainState).options
   let (fileName, file) ← match args.fileName?, args.file? with