Main.lean

@@ -33,16 +33,11 @@ partial def loop : MainM Unit := do
     -- Using `Lean.Json.compress` here to prevent newline
     IO.println error.compress
   | .ok command =>
-    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
-      IO.println str
-    catch e =>
-      let message ← e.toMessageData.toString
-      let error  := Lean.toJson ({ error := "main", desc := message }: InteractionError)
-      IO.println error.compress
   loop
 
 
@@ -50,7 +45,7 @@ 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
-    IO.println s!"{Pantograph.version}"
+    println! s!"{Pantograph.version}"
     return
 
   Pantograph.initSearch ""
@@ -67,6 +62,5 @@ unsafe def main (args: List String): IO Unit := do
     IO.println "ready."
     discard <| coreM.toIO coreContext coreState
   catch ex =>
-    let message := ex.toString
+    IO.println "Uncaught IO exception"
-    let error  := Lean.toJson ({ error := "io", desc := message }: InteractionError)
+    IO.println ex.toString
-    IO.println error.compress