improve custom goal display

client/src/components/Infoview.tsx

@@ -11,43 +11,63 @@ function toLanguageServerPosition (pos: monaco.Position): ls.Position {
   return {line : pos.lineNumber - 1, character: pos.column - 1}
 }
 
-function Infoview({ ready, editor, editorApi, uri, leanClient } : {ready: boolean, editor: monaco.editor.IStandaloneCodeEditor, editorApi: EditorApi, uri: any, leanClient: LeanClient}) {
+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 liftOff = async () => {
-    const rpcSession = await editorApi.createRpcSession(uri)
-    const fetchInteractiveGoals = () => {
+  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,
         "textDocument":{uri},
         "position": pos
-      }).then(({ goals }) => {
-        setGoals(goals)
+      }).then((res) => {
+        setGoals(res ? res.goals : null)
         console.log(goals)
       }).catch((err) => {
         console.error(err)
       })
     }
-    setRpcSession(rpcSession)
-    editor.onDidChangeCursorPosition((ev) => {
-      fetchInteractiveGoals()
-    })
-    leanClient.didChange(async (ev) => {
-      fetchInteractiveGoals()
-    })
   }
 
   useEffect(() => {
-    if (ready) {
-      liftOff()
+    if (editor) {
+      const t = editor.onDidChangeModel((ev) => {
+        if (ev.newModelUrl) {
+          setRpcSession(undefined)
+          setUri(ev.newModelUrl.toString())
+          editorApi.createRpcSession(ev.newModelUrl.toString()).then((rpcSession) => {
+            setRpcSession(rpcSession)
+            fetchInteractiveGoals()
+          })
+        }
+      })
+      return () => {t.dispose()}
     }
-  }, [ready])
-   // Lean.Widget.getInteractiveGoals
+  }, [editor, rpcSession]);
+
+  useEffect(() => {
+    if (editor) {
+      const t = editor.onDidChangeCursorPosition(async (ev) => {
+        fetchInteractiveGoals()
+      })
+      return () => { t.dispose() }
+    }
+  }, [editor, rpcSession])
+
+  useEffect(() => {
+    const t = leanClient.didChange(async (ev) => {
+      fetchInteractiveGoals()
+    })
+    return () => { t.dispose() }
+  }, [editor, leanClient, rpcSession])
 
   return (<div>
-    <TacticState goals={goals} errors={[]} completed={false}></TacticState>
+    <TacticState goals={goals} errors={[]} completed={goals?.length === 0}></TacticState>
   </div>)
 }
 

client/src/components/Level.tsx

@@ -7,7 +7,7 @@ import '@fontsource/roboto/700.css';
 import ReactMarkdown from 'react-markdown';
 import { MathJax } from "better-react-mathjax";
 
-import { Button } from '@mui/material';
+import { Button, FormControlLabel, FormGroup, Switch } from '@mui/material';
 import Grid from '@mui/material/Unstable_Grid2';
 
 import LeftPanel from './LeftPanel';
@@ -40,6 +40,8 @@ function Level({ nbLevels, level, setCurLevel, setLevelTitle, setFinished }: Lev
   const [editor, setEditor] = useState<monaco.editor.IStandaloneCodeEditor|null>(null)
   const [infoProvider, setInfoProvider] = useState<null|InfoProvider>(null)
   const [infoviewApi, setInfoviewApi] = useState(null)
+  const [expertInfoview, setExpertInfoview] = useState(false)
+
 
   const [leanData, setLeanData] = useState({goals: []})
   const [history, setHistory] = useState([])
@@ -129,7 +131,7 @@ function Level({ nbLevels, level, setCurLevel, setLevelTitle, setFinished }: Lev
         processResponse(res)
       });
 
-      return () => { model.dispose(); }
+      return () => { model.dispose(); setReady(false) }
     }
   }, [editor, level, leanClient])
 
@@ -157,9 +159,13 @@ function Level({ nbLevels, level, setCurLevel, setLevelTitle, setFinished }: Lev
       <Grid xs={4} className="info-panel">
         <Button disabled={index <= 1} onClick={() => { loadLevel(index - 1) }} sx={{ ml: 3, mt: 2, mb: 2 }} disableFocusRipple>Previous Level</Button>
         <Button disabled={index >= nbLevels} onClick={() => { loadLevel(index + 1) }} sx={{ ml: 3, mt: 2, mb: 2 }} disableFocusRipple>Next Level</Button>
-        <div ref={infoviewRef} className="infoview vscode-light"></div>
-        <Infoview ready={ready} leanClient={leanClient} editor={editor} editorApi={infoProvider?.getApi()} uri={uri} />
-        {/* <TacticState goals={leanData.goals} errors={errors} lastTactic={lastTactic} completed={completed} /> */}
+        <div style={{display: expertInfoview ? 'block' : 'none' }} ref={infoviewRef} className="infoview vscode-light"></div>
+        <div style={{display: expertInfoview ? 'none' : 'block' }}>
+          <Infoview leanClient={leanClient} editor={editor} editorApi={infoProvider?.getApi()} />
+        </div>
+        <FormGroup>
+          <FormControlLabel onChange={() => { setExpertInfoview(!expertInfoview) }} control={<Switch />} label="Expert mode" />
+        </FormGroup>
       </Grid>
     </Grid>
   )

client/src/components/TacticState.tsx

@@ -25,8 +25,8 @@ function Goal({ goal }) {
         </List></Box>}
       {hasAssumption && <Box><Typography>Assumptions</Typography>
         <List>
-          {goal.assumptions.map((item) => <ListItem key={item}><Typography color="primary" sx={{ mr: 1 }}>{item[0]}</Typography> :
-            <Typography color="secondary" sx={{ ml: 1 }}>{item[1]}</Typography></ListItem>)}
+          {goal.assumptions.map((item) => <ListItem key={item}><Typography color="primary" sx={{ mr: 1 }}>{item.userName}</Typography> :
+            <Typography color="secondary" sx={{ ml: 1 }}>{item.type}</Typography></ListItem>)}
         </List></Box>}
       <Typography>Prove:</Typography>
       <Typography color="primary" sx={{ ml: 2 }}>{goal.goal}</Typography>
@@ -51,7 +51,8 @@ function TacticState({ goals, errors, completed }) {
   }
   return (
     <Box sx={{ height: "100%" }}>
-      {hasGoal && <Paper sx={{ pt: 1, pl: 2, pr: 3, pb: 1, height: "100%" }}><Typography variant="h5">Current goal</Typography> <Goal goal={goals[0]} /></Paper>}
+      {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>
         <Typography component="pre" sx={{ my: 1 }}>{col}{msg}</Typography>