Main.lean

@@ -8,12 +8,6 @@ import Repl
 open Pantograph.Repl
 open Pantograph.Protocol
 
-/-- Print a string to stdout without buffering -/
-def printImmediate (s : String) : IO Unit := do
-  let stdout ← IO.getStdout
-  stdout.putStr (s ++ "\n")
-  stdout.flush
-
 /-- Parse a command either in `{ "cmd": ..., "payload": ... }` form or `cmd { ... }` form. -/
 def parseCommand (s: String): Except String Command := do
   match s.trim.get? 0 with
@@ -40,26 +34,26 @@ partial def loop : MainM Unit := do repeat do
   | .error error =>
     let error  := Lean.toJson ({ error := "command", desc := error }: InteractionError)
     -- Using `Lean.Json.compress` here to prevent newline
-    printImmediate error.compress
+    IO.println error.compress
   | .ok command =>
     try
       let ret ← execute command
       let str := match state.options.printJsonPretty with
         | true => ret.pretty
         | false => ret.compress
-      printImmediate str
+      IO.println str
     catch e =>
       let message := e.toString
       let error  := Lean.toJson ({ error := "main", desc := message }: InteractionError)
-      printImmediate error.compress
+      IO.println error.compress
 
-def main (args: List String): IO Unit := do
+
+unsafe def main (args: List String): IO Unit := do
   -- NOTE: A more sophisticated scheme of command line argument handling is needed.
   if args == ["--version"] then do
     IO.println s!"{Pantograph.version}"
     return
 
-  unsafe do
   Pantograph.initSearch ""
 
   -- Separate imports and options
@@ -68,7 +62,7 @@ def main (args: List String): IO Unit := do
   let coreState ← Pantograph.createCoreState imports.toArray
   try
     let mainM := loop.run { coreContext } |>.run' { env := coreState.env }
-    printImmediate "ready."
+    IO.println "ready."
     mainM
   catch ex =>
     let message := ex.toString