From bec84f857bd4f80064213fa5646bef4699191290 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 9 Sep 2024 18:43:34 -0700
Subject: [PATCH] fix: repl build failure

---
 Main.lean | 15 +++++++--------
 1 file changed, 7 insertions(+), 8 deletions(-)

diff --git a/Main.lean b/Main.lean
index 2959a64..b866711 100644
--- a/Main.lean
+++ b/Main.lean
@@ -1,16 +1,15 @@
 import Lean.Data.Json
 import Lean.Environment
 
-import Pantograph.Version
-import Pantograph.Library
 import Pantograph
 import Repl
 
 -- Main IO functions
 open Pantograph.Repl
+open Pantograph.Protocol
 
 /-- Parse a command either in `{ "cmd": ..., "payload": ... }` form or `cmd { ... }` form. -/
-def parseCommand (s: String): Except String Protocol.Command := do
+def parseCommand (s: String): Except String Command := do
   let s := s.trim
   match s.get? 0 with
   | .some '{' => -- Parse in Json mode
@@ -30,7 +29,7 @@ partial def loop : MainM Unit := do
   if command.trim.length = 0 then return ()
   match parseCommand command with
   | .error error =>
-    let error  := Lean.toJson ({ error := "command", desc := error }: Protocol.InteractionError)
+    let error  := Lean.toJson ({ error := "command", desc := error }: InteractionError)
     -- Using `Lean.Json.compress` here to prevent newline
     IO.println error.compress
   | .ok command =>
@@ -46,15 +45,15 @@ unsafe def main (args: List String): IO Unit := do
   -- NOTE: A more sophisticated scheme of command line argument handling is needed.
   -- Separate imports and options
   if args == ["--version"] then do
-    println! s!"{version}"
+    println! s!"{Pantograph.version}"
     return
 
-  initSearch ""
+  Pantograph.initSearch ""
 
   let coreContext ← args.filterMap (λ s => if s.startsWith "--" then .some <| s.drop 2 else .none)
-    |>.toArray |> createCoreContext
+    |>.toArray |> Pantograph.createCoreContext
   let imports:= args.filter (λ s => ¬ (s.startsWith "--"))
-  let coreState ← createCoreState imports.toArray
+  let coreState ← Pantograph.createCoreState imports.toArray
   let context: Context := {
     imports
   }