feat: Catch IO errors in json format

This commit is contained in:
Leni Aniva 2024-10-08 00:45:45 -07:00
parent 5e776a1b49
commit 05d0b7739a
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
1 changed files with 5 additions and 4 deletions

View File

@ -41,7 +41,7 @@ partial def loop : MainM Unit := do
IO.println str IO.println str
catch e => catch e =>
let message ← e.toMessageData.toString let message ← e.toMessageData.toString
let error := Lean.toJson ({ error := "io", desc := message }: InteractionError) let error := Lean.toJson ({ error := "main", desc := message }: InteractionError)
IO.println error.compress IO.println error.compress
loop loop
@ -50,7 +50,7 @@ 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.
-- Separate imports and options -- Separate imports and options
if args == ["--version"] then do if args == ["--version"] then do
println! s!"{Pantograph.version}" IO.println s!"{Pantograph.version}"
return return
Pantograph.initSearch "" Pantograph.initSearch ""
@ -67,5 +67,6 @@ unsafe def main (args: List String): IO Unit := do
IO.println "ready." IO.println "ready."
discard <| coreM.toIO coreContext coreState discard <| coreM.toIO coreContext coreState
catch ex => 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