merge

client/src/components/Level.tsx

@@ -45,13 +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: 0, ml: 0, mr: 0 }} columnSpacing={{ xs: 1, sm: 2, md: 3 }}>
-      <Grid xs={0} sm={3} className="doc-panel">
+      <Grid xs={4} className="doc-panel">
         <LeftPanel spells={level?.data?.tactics} inventory={level?.data?.tactics} />
       </Grid>
       <Grid xs={9} sm={6} className="main-panel">

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

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,