From 8adab241577031000d25ee5e77909f5dd707baf5 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 28 Mar 2025 00:56:18 -0700
Subject: [PATCH] fix: Call sites in `Main.lean`

---
 Main.lean | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/Main.lean b/Main.lean
index c4d30c6..4e3ae33 100644
--- a/Main.lean
+++ b/Main.lean
@@ -43,7 +43,7 @@ partial def loop : MainM Unit := do repeat do
         | false => ret.compress
       IO.println str
     catch e =>
-      let message ← e.toMessageData.toString
+      let message := e.toString
       let error  := Lean.toJson ({ error := "main", desc := message }: InteractionError)
       IO.println error.compress
 
@@ -60,11 +60,10 @@ unsafe def main (args: List String): IO Unit := do
   let (options, imports) := args.partition (·.startsWith "--")
   let coreContext ← options.map (·.drop 2) |>.toArray |> Pantograph.createCoreContext
   let coreState ← Pantograph.createCoreState imports.toArray
-  let context: Context := {}
   try
-    let coreM := loop.run context |>.run' {}
+    let mainM := loop.run { coreContext } |>.run' { env := coreState.env }
     IO.println "ready."
-    discard <| coreM.toIO coreContext coreState
+    mainM
   catch ex =>
     let message := ex.toString
     let error  := Lean.toJson ({ error := "io", desc := message }: InteractionError)