diagnostics for simple infoview

client/src/components/Infoview.tsx

@@ -14,12 +14,13 @@ 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 [uri, setUri] = useState<string>()
   console.log(rpcSession)
   const fetchInteractiveGoals = () => {
-    console.log(rpcSession)
     if (editor && rpcSession) {
       const pos = toLanguageServerPosition(editor.getPosition())
+
       leanClient.sendRequest("$/lean/rpc/call", {"method":"Game.getGoals",
         "params":{"textDocument":{uri}, "position": pos},
         "sessionId":rpcSession,
@@ -31,6 +32,19 @@ function Infoview({ editor, editorApi, leanClient } : {editor: monaco.editor.ISt
       }).catch((err) => {
         console.error(err)
       })
+
+      leanClient.sendRequest("$/lean/rpc/call", {"method":"Game.getDiagnostics",
+        "params":{"textDocument":{uri}, "position": pos},
+        "sessionId":rpcSession,
+        "textDocument":{uri},
+        "position": pos
+      }).then((res) => {
+        setErrors(res ? res : undefined)
+        console.log(res)
+      }).catch((err) => {
+        console.error(err)
+      })
+
     }
   }
 
@@ -67,7 +81,7 @@ function Infoview({ editor, editorApi, leanClient } : {editor: monaco.editor.ISt
   }, [editor, leanClient, rpcSession])
 
   return (<div>
-    <TacticState goals={goals} errors={[]} completed={goals?.length === 0}></TacticState>
+    <TacticState goals={goals} errors={errors} completed={goals?.length === 0 && errors?.length === 0}></TacticState>
   </div>)
 }
 

client/src/components/TacticState.tsx

@@ -9,7 +9,6 @@ import { MathJax } from "better-react-mathjax";
 import List from '@mui/material/List';
 import ListItem from '@mui/material/ListItem';
 import { Paper, Box, Typography, Alert, FormControlLabel, FormGroup, Switch, Collapse } from '@mui/material';
-const errorRegex = /<stdin>:1:(?<col>[^:]*): (?<msg>.*)/;
 
 // TODO: Dead variables (x✝) are not displayed correctly.
 
@@ -57,26 +56,13 @@ function TacticState({ goals, errors, completed }) {
   const hasError = typeof errors === "object" && errors.length > 0
   const hasGoal = goals !== null && goals.length > 0
   const hasManyGoal = hasGoal && goals.length > 1
-  var col = ""
-  var msg = ""
-  if (hasError) {
-    const m = errors[0].match(errorRegex)
-    if (m) {
-      col = `Column ${m.groups.col}: `
-      msg = m.groups.msg
-    } else {
-      msg = errors[0]
-      if (msg === "Unrecognized tactic") { msg = "Unknown spell!" }
-    }
-  }
   return (
     <Box sx={{ height: "100%" }}>
       {goals === null && <Typography variant="h6">No goals at cursor position</Typography>}
       {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%" }}><Typography variant="h5" color="error">Spell invocation failed</Typography>
+      {hasError && <Paper sx={{ pt: 1, pl: 2, pr: 3, pb: 1, height: "100%" }}>
-        <Typography component="pre" sx={{ my: 1 }}>{col}{msg}</Typography>
+        {errors.map(({severity, message}) => <Typography color={{1: "red", 2:"orange", 3:"blue", 4:"gray"}[severity]}>{message}</Typography>)}
-        <Typography>Use the undo button to go back to a sane state.</Typography>
         </Paper>}
       {hasManyGoal && <Paper sx={{ pt: 1, pl: 2, pr: 3, pb: 1, mt: 1 }}>
         <Typography variant="h6" sx={{ mb: 2 }}>Other goals</Typography>

server/leanserver/GameServer/RpcHandlers.lean

@@ -147,4 +147,34 @@ builtin_initialize
     (Option PlainGoal)
     getGoals
 
+
+structure Diagnostic where
+  severity : Option Lean.Lsp.DiagnosticSeverity
+  message : String
+deriving FromJson, ToJson
+
+open RequestM in
+def getDiagnostics (params : GetInteractiveDiagnosticsParams) : RequestM (RequestTask (Array Diagnostic)) := do
+  let doc ← readDoc
+  let rangeEnd := params.lineRange?.map fun range =>
+    doc.meta.text.lspPosToUtf8Pos ⟨range.«end», 0⟩
+  let t := doc.cmdSnaps.waitAll fun snap => rangeEnd.all (snap.beginPos < ·)
+  pure <| t.map fun (snaps, _) =>
+    let diags? := snaps.getLast?.map fun snap =>
+      snap.interactiveDiags.toArray.filterMap fun diag =>
+        if params.lineRange?.all fun ⟨s, e⟩ =>
+          -- does [s,e) intersect [diag.fullRange.start.line,diag.fullRange.end.line)?
+          s ≤ diag.fullRange.start.line ∧ diag.fullRange.start.line < e ∨
+          diag.fullRange.start.line ≤ s ∧ s < diag.fullRange.end.line
+        then some {message := diag.message.stripTags, severity := diag.severity?}
+        else none
+    pure <| diags?.getD #[]
+
+builtin_initialize
+  registerBuiltinRpcProcedure
+    `Game.getDiagnostics
+    GetInteractiveDiagnosticsParams
+    (Array Diagnostic)
+    getDiagnostics
+
 end GameServer