From 4bb44dd56a8072d69db6f9be82bdde54ca807f0e Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 2 May 2025 11:33:11 -0400
Subject: [PATCH] chore: Syntax cleanup in repl

---
 Repl.lean | 15 ++++++---------
 1 file changed, 6 insertions(+), 9 deletions(-)

diff --git a/Repl.lean b/Repl.lean
index 6a03cbe..4c9ddf2 100644
--- a/Repl.lean
+++ b/Repl.lean
@@ -39,7 +39,7 @@ def newGoalState (goalState : GoalState) : MainM Nat := do
 
 def runCoreM { α } (coreM : CoreM α) : EMainM α := do
   let scope := (← get).scope
-  let options :=(← get).options
+  let options := (← get).options
   let cancelTk? ← match options.timeout with
     | 0 => pure .none
     | _ => .some <$> IO.CancelToken.new
@@ -60,7 +60,7 @@ def runCoreM { α } (coreM : CoreM α) : EMainM α := do
       Except.ok <$> coreM
     catch ex =>
       let desc ← ex.toMessageData.toString
-      return Except.error $ ({ error := "exception", desc } : Protocol.InteractionError)
+      return Except.error ({ error := "exception", desc } : Protocol.InteractionError)
     finally
       for {msg, ..} in (← getTraceState).traces do
         IO.eprintln (← msg.format.toIO)
@@ -72,16 +72,15 @@ def runCoreM { α } (coreM : CoreM α) : EMainM α := do
     | Except.error (Exception.internal id _) => Protocol.throw $ { error := "internal", desc := (← id.getName).toString }
     | Except.ok a                            => pure a
   if result matches .ok _ then
-    modifyEnv λ _ => state'.env
+    setEnv state'.env
   liftExcept result
 
 def runCoreM' { α } (coreM : Protocol.FallibleT CoreM α) : EMainM α := do
   liftExcept $ ← runCoreM coreM.run
 
-
 def liftMetaM { α } (metaM : MetaM α): EMainM α :=
   runCoreM metaM.run'
-def liftTermElabM { α } (termElabM: Elab.TermElabM α) (levelNames : List Name := [])
+def liftTermElabM { α } (termElabM : Elab.TermElabM α) (levelNames : List Name := [])
     : EMainM α := do
   let scope := (← get).scope
   let context := {
@@ -96,7 +95,7 @@ def liftTermElabM { α } (termElabM: Elab.TermElabM α) (levelNames : List Name
 section Frontend
 
 structure CompilationUnit where
-  -- Should be the penultimate environment, but this is ok
+  -- Environment immediately before the unit
   env : Environment
   boundary : Nat × Nat
   invocations : List Protocol.InvokedTactic
@@ -104,7 +103,7 @@ structure CompilationUnit where
   messages : Array String
   newConstants : List Name
 
-def frontend_process_inner (args: Protocol.FrontendProcess): EMainM Protocol.FrontendProcessResult := do
+def frontend_process (args: Protocol.FrontendProcess): EMainM Protocol.FrontendProcessResult := do
   let options := (← getMainState).options
   let (fileName, file) ← match args.fileName?, args.file? with
     | .some fileName, .none => do
@@ -400,7 +399,5 @@ def execute (command: Protocol.Command): MainM Json := do
     let (goalState, _) ← goalStateUnpickle args.path (← MonadEnv.getEnv)
     let id ← newGoalState goalState
     return { id }
-  frontend_process (args: Protocol.FrontendProcess): EMainM Protocol.FrontendProcessResult := do
-    frontend_process_inner args
 
 end Pantograph.Repl