reliable level completed message

client/src/components/Infoview.tsx

@@ -14,7 +14,8 @@ function toLanguageServerPosition (pos: monaco.Position): ls.Position {
 function Infoview({ editor, editorApi, leanClient } : {editor: monaco.editor.IStandaloneCodeEditor, editorApi: EditorApi, leanClient: LeanClient}) {
   const [rpcSession, setRpcSession] = useState<string>()
   const [goals, setGoals] = useState<any[]>(null)
-  const [errors, setErrors] = useState<any[]>(undefined)
+  const [completed, setCompleted] = useState<boolean>(false)
+  const [diagnostics, setDiagnostics] = useState<any[]>(undefined)
   const [uri, setUri] = useState<string>()
   console.log(rpcSession)
   const fetchInteractiveGoals = () => {
@@ -34,12 +35,12 @@ function Infoview({ editor, editorApi, leanClient } : {editor: monaco.editor.ISt
       })
 
       leanClient.sendRequest("$/lean/rpc/call", {"method":"Game.getDiagnostics",
-        "params":{"textDocument":{uri}, "position": pos},
+        "params":{"textDocument":{uri}, "lineRange": {start: pos.line, end: pos.line + 1}},
         "sessionId":rpcSession,
         "textDocument":{uri},
         "position": pos
       }).then((res) => {
-        setErrors(res ? res : undefined)
+        setDiagnostics(res ? res : undefined)
         console.log(res)
       }).catch((err) => {
         console.error(err)
@@ -48,6 +49,22 @@ function Infoview({ editor, editorApi, leanClient } : {editor: monaco.editor.ISt
     }
   }
 
+  const checkCompleted = () => {
+    const pos = toLanguageServerPosition(editor.getPosition())
+    // Get all diagnostics independent of cursor position
+    leanClient.sendRequest("$/lean/rpc/call", {"method":"Game.getDiagnostics",
+      "params":{"textDocument":{uri},},
+      "sessionId":rpcSession,
+      "textDocument":{uri},
+      "position": pos
+    }).then((res) => {
+      // Check that there are no errors and no warnings
+      setCompleted(!res.some(({severity}) => severity <= 2))
+    }).catch((err) => {
+      console.error(err)
+    })
+  }
+
   useEffect(() => {
     if (editor) {
       fetchInteractiveGoals()
@@ -76,12 +93,13 @@ function Infoview({ editor, editorApi, leanClient } : {editor: monaco.editor.ISt
   useEffect(() => {
     const t = leanClient.didChange(async (ev) => {
       fetchInteractiveGoals()
+      checkCompleted()
     })
     return () => { t.dispose() }
   }, [editor, leanClient, rpcSession])
 
   return (<div>
-    <TacticState goals={goals} errors={errors} completed={goals?.length === 0 && errors?.length === 0}></TacticState>
+    <TacticState goals={goals} diagnostics={diagnostics} completed={completed}></TacticState>
   </div>)
 }
 

client/src/components/TacticState.tsx

@@ -52,8 +52,8 @@ function Goal({ goal }) {
     </Box>)
 }
 
-function TacticState({ goals, errors, completed }) {
-  const hasError = typeof errors === "object" && errors.length > 0
+function TacticState({ goals, diagnostics, completed }) {
+  const hasError = typeof diagnostics === "object" && diagnostics.length > 0
   const hasGoal = goals !== null && goals.length > 0
   const hasManyGoal = hasGoal && goals.length > 1
   return (
@@ -62,7 +62,7 @@ function TacticState({ goals, errors, completed }) {
       {hasGoal && <Paper sx={{ pt: 1, pl: 2, pr: 3, pb: 1, height: "100%" }}><Typography variant="h5">Main goal at cursor</Typography> <Goal goal={goals[0]} /></Paper>}
       {completed && <Typography variant="h6">Level completed ! 🎉</Typography>}
       {hasError && <Paper sx={{ pt: 1, pl: 2, pr: 3, pb: 1, height: "100%" }}>
-        {errors.map(({severity, message}) => <Typography color={{1: "red", 2:"orange", 3:"blue", 4:"gray"}[severity]}>{message}</Typography>)}
+        {diagnostics.map(({severity, message}) => <Typography color={{1: "red", 2:"orange", 3:"blue", 4:"gray"}[severity]}>{message}</Typography>)}
         </Paper>}
       {hasManyGoal && <Paper sx={{ pt: 1, pl: 2, pr: 3, pb: 1, mt: 1 }}>
         <Typography variant="h6" sx={{ mb: 2 }}>Other goals</Typography>