reinsert vscode infoview

client/src/components/Level.tsx

@@ -4,6 +4,7 @@ import '@fontsource/roboto/300.css';
 import '@fontsource/roboto/400.css';
 import '@fontsource/roboto/500.css';
 import '@fontsource/roboto/700.css';
+import { InfoviewApi, renderInfoview } from '@leanprover/infoview'
 import { Link as RouterLink } from 'react-router-dom';
 import { Box, Button, CircularProgress, FormControlLabel, FormGroup, Switch, IconButton } from '@mui/material';
 import MuiDrawer from '@mui/material/Drawer';
@@ -131,7 +132,7 @@ function Level() {
   const initialCode = useSelector(selectCode(worldId, levelId))
 
   const {editor, infoProvider} =
-    useLevelEditor(worldId, levelId, codeviewRef, initialCode, onDidChangeContent)
+    useLevelEditor(worldId, levelId, codeviewRef, infoviewRef, initialCode, onDidChangeContent)
 
   const {setTitle, setSubtitle} = React.useContext(SetTitleContext);
 
@@ -185,7 +186,8 @@ function Level() {
             component={RouterLink} to={`/`}
             sx={{ ml: 3, mt: 2, mb: 2 }} disableFocusRipple><FontAwesomeIcon icon={faHome}></FontAwesomeIcon></Button>
 
-          <Infoview key={worldId + "/Level" + levelId} worldId={worldId} levelId={levelId} editor={editor} editorApi={infoProvider?.getApi()} />
+          <div ref={infoviewRef} className="infoview vscode-light"></div>
+          {/* <Infoview key={worldId + "/Level" + levelId} worldId={worldId} levelId={levelId} editor={editor} editorApi={infoProvider?.getApi()} /> */}
         </Grid>
       </Grid>
     </Box>
@@ -195,12 +197,13 @@ function Level() {
 export default Level
 
 
-function useLevelEditor(worldId: string, levelId: number, codeviewRef, initialCode, onDidChangeContent) {
+function useLevelEditor(worldId: string, levelId: number, codeviewRef, infoviewRef, initialCode, onDidChangeContent) {
 
   const connection = React.useContext(ConnectionContext)
 
   const [editor, setEditor] = useState<monaco.editor.IStandaloneCodeEditor|null>(null)
   const [infoProvider, setInfoProvider] = useState<null|InfoProvider>(null)
+  const [infoviewApi, setInfoviewApi] = useState<null|InfoviewApi>(null)
 
   // Create Editor
   useEffect(() => {
@@ -222,9 +225,12 @@ function useLevelEditor(worldId: string, levelId: number, codeviewRef, initialCo
     })
 
     const infoProvider = new InfoProvider(connection.getLeanClient())
+    const div: HTMLElement = infoviewRef.current!
+    const infoviewApi = renderInfoview(infoProvider.getApi(), div)
 
     setEditor(editor)
     setInfoProvider(infoProvider)
+    setInfoviewApi(infoviewApi)
 
     return () => { editor.setModel(null); infoProvider.dispose(); editor.dispose() }
   }, [])
@@ -243,6 +249,10 @@ function useLevelEditor(worldId: string, levelId: number, codeviewRef, initialCo
       }
       editor.setModel(model)
       editor.setPosition(model.getFullModelRange().getEndPosition())
+
+      infoviewApi.serverRestarted(leanClient.initializeResult)
+      infoProvider.openPreview(editor, infoviewApi)
+
       const taskGutter = new LeanTaskGutter(infoProvider.client, editor)
       const abbrevRewriter = new AbbreviationRewriter(new AbbreviationProvider(), model, editor)