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