From 0ec9cadb13a39e79c95df0fe359b77b4e6b026e2 Mon Sep 17 00:00:00 2001
From: Alexander Bentkamp <bentkamp@gmail.com>
Date: Tue, 13 Dec 2022 11:02:32 +0100
Subject: [PATCH] display errors

---
 client/src/components/Level.tsx        |  4 ++--
 client/src/game/api.ts                 | 16 ++++++++++------
 server/leanserver/GameServer/Game.lean |  4 +++-
 3 files changed, 15 insertions(+), 9 deletions(-)

diff --git a/client/src/components/Level.tsx b/client/src/components/Level.tsx
index 9ecad39..85991e7 100644
--- a/client/src/components/Level.tsx
+++ b/client/src/components/Level.tsx
@@ -45,12 +45,12 @@ function Level() {
   const connection = React.useContext(ConnectionContext)
 
   const level = useLoadLevelQuery({world: worldId, level: levelId})
-
   const {editor, infoProvider} = useLevelEditor(worldId, levelId, codeviewRef, infoviewRef)
 
   return <>
     <Box style={level.isLoading ? null : {display: "none"}} display="flex" alignItems="center" justifyContent="center" sx={{ height: "calc(100vh - 64px)" }}><CircularProgress /></Box>
-    <Grid style={level.isLoading ? {display: "none"} : null} className="level" container sx={{ mt: 3, ml: 1, mr: 1 }} columnSpacing={{ xs: 1, sm: 2, md: 3 }}>
+    <Box style={level.isError ? null : {display: "none"}} display="flex" alignItems="center" justifyContent="center" sx={{ height: "calc(100vh - 64px)" }}>{level?.error?.message}</Box>
+    <Grid style={level.isLoading || level.isError ? {display: "none"} : null} className="level" container sx={{ mt: 3, ml: 1, mr: 1 }} columnSpacing={{ xs: 1, sm: 2, md: 3 }}>
       <Grid xs={4} className="doc-panel">
         <LeftPanel spells={level?.data?.tactics} inventory={level?.data?.tactics} />
       </Grid>
diff --git a/client/src/game/api.ts b/client/src/game/api.ts
index 739b11b..784cfd7 100644
--- a/client/src/game/api.ts
+++ b/client/src/game/api.ts
@@ -24,12 +24,16 @@ const customBaseQuery = async (
   { signal, dispatch, getState, extra },
   extraOptions
 ) => {
-  const connection : Connection = extra.connection
-  let leanClient = await connection.startLeanClient()
-  console.log(`Sending request ${args.method}`)
-  let res = await leanClient.sendRequest(args.method, args.params)
-  console.log('Received response', res)
-  return {'data': res}
+  try {
+    const connection : Connection = extra.connection
+    let leanClient = await connection.startLeanClient()
+    console.log(`Sending request ${args.method}`)
+    let res = await leanClient.sendRequest(args.method, args.params)
+    console.log('Received response', res)
+    return {'data': res}
+   } catch (e) {
+    return {'error': e}
+   }
 }
 
 // Define a service using a base URL and expected endpoints
diff --git a/server/leanserver/GameServer/Game.lean b/server/leanserver/GameServer/Game.lean
index b95161d..b709fb4 100644
--- a/server/leanserver/GameServer/Game.lean
+++ b/server/leanserver/GameServer/Game.lean
@@ -64,7 +64,9 @@ partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do
       let s ← get
       let c ← read
       let some lvl ← getLevel? {game := s.game, world := p.world, level := p.level}
-        | throwServerError s!"Level not found {(← getGame s.game).name} {p.world} {p.level}"
+        | do
+            c.hOut.writeLspResponseError ⟨id, .invalidParams, s!"Level not found: world {p.world}, level {p.level}", none⟩
+            return true
       let levelInfo : LevelInfo :=
           { index := lvl.index,
             title := lvl.title,