Main.lean

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