better error messages

LeanSearchClient/LoogleSyntax.lean

@@ -57,8 +57,8 @@ def getLoogleQueryJson (s : String) (num_results : Nat := 6) :
   let q := apiUrl ++ s!"?q={s'}"
   let s ← IO.Process.output {cmd := "curl", args := #["-X", "GET", "--user-agent", ← useragent,  q]}
   match Json.parse s.stdout with
-  | Except.error e =>
-    IO.throwServerError s!"Could not parse JSON from {s.stdout}; error: {e}"
+  | Except.error _ =>
+    IO.throwServerError s!"Could not contact Loogle server"
   | Except.ok js =>
   let result? := js.getObjValAs?  Json "hits" |>.toOption
   let result? := result?.filter fun js => js != Json.null

LeanSearchClient/Syntax.lean

@@ -45,17 +45,19 @@ def getLeanSearchQueryJson (s : String) (num_results : Nat := 6) : CoreM <| Arra
   let s' := System.Uri.escapeUri s
   let q := apiUrl ++ s!"?query={s'}&num_results={num_results}"
   let s ← IO.Process.output {cmd := "curl", args := #["-X", "GET", "--user-agent", ← useragent, q]}
-  let js := Json.parse s.stdout |>.toOption |>.get!
-  return js.getArr? |>.toOption |>.get!
+  let js ← match Json.parse s.stdout |>.toOption with
+    | some js => pure js
+    | none => IO.throwServerError s!"Could not contact LeanSearch server"
+  return js.getArr? |>.toOption |>.getD #[]
 
 def getMoogleQueryJson (s : String) (num_results : Nat := 6) : CoreM <| Array Json := do
   let apiUrl := "https://www.moogle.ai/api/search"
   let data := Json.arr
     #[Json.mkObj [("isFind", false), ("contents", s)]]
   let s ← IO.Process.output {cmd := "curl", args := #[apiUrl, "-H", "content-type: application/json",  "--user-agent", ← useragent, "--data", data.pretty]}
   match Json.parse s.stdout with
-  | Except.error e =>
-    IO.throwServerError s!"Could not parse JSON from {s.stdout}; error: {e}"
+  | Except.error _ =>
+    throwError m!"Could not contact Moogle server"
   | Except.ok js =>
   let result? := js.getObjValAs?  Json "data"
   match result? with