move renderInfoview function

client/src/components/Level.tsx

@@ -5,7 +5,7 @@ import '@fontsource/roboto/400.css';
 import '@fontsource/roboto/500.css';
 import '@fontsource/roboto/700.css';
 import { InfoviewApi } from '@leanprover/infoview'
-import { renderInfoview } from './infoview/main'
+import * as ReactDOM from 'react-dom/client';
 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';
@@ -28,6 +28,12 @@ import { codeEdited, selectCode } from '../state/progress';
 import { useAppDispatch } from '../hooks';
 import { useSelector } from 'react-redux';
 
+import { EditorContext, ConfigContext, ProgressContext, VersionContext } from '../../../node_modules/lean4-infoview/src/infoview/contexts';
+import { EditorConnection, EditorEvents } from '../../../node_modules/lean4-infoview/src/infoview/editorConnection';
+import { EventEmitter } from '../../../node_modules/lean4-infoview/src/infoview/event';
+import { Main } from './infoview/main'
+import type { Location } from 'vscode-languageserver-protocol';
+
 import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
 import { faUpload, faArrowRotateRight, faChevronLeft, faChevronRight, faBook, faHome, faArrowRight, faArrowLeft } from '@fortawesome/free-solid-svg-icons'
 
@@ -228,8 +234,54 @@ function useLevelEditor(worldId: string, levelId: number, codeviewRef, infoviewR
     })
 
     const infoProvider = new InfoProvider(connection.getLeanClient())
-    const div: HTMLElement = infoviewRef.current!
-    const infoviewApi = renderInfoview(infoProvider.getApi(), div)
+    const uiElement: HTMLElement = infoviewRef.current!
+
+    const editorApi = infoProvider.getApi()
+
+    const editorEvents: EditorEvents = {
+        initialize: new EventEmitter(),
+        gotServerNotification: new EventEmitter(),
+        sentClientNotification: new EventEmitter(),
+        serverRestarted: new EventEmitter(),
+        serverStopped: new EventEmitter(),
+        changedCursorLocation: new EventEmitter(),
+        changedInfoviewConfig: new EventEmitter(),
+        runTestScript: new EventEmitter(),
+        requestedAction: new EventEmitter(),
+    };
+
+    // Challenge: write a type-correct fn from `Eventify<T>` to `T` without using `any`
+    const infoviewApi: InfoviewApi = {
+        initialize: async l => editorEvents.initialize.fire(l),
+        gotServerNotification: async (method, params) => {
+            editorEvents.gotServerNotification.fire([method, params]);
+        },
+        sentClientNotification: async (method, params) => {
+            editorEvents.sentClientNotification.fire([method, params]);
+        },
+        serverRestarted: async r => editorEvents.serverRestarted.fire(r),
+        serverStopped: async serverStoppedReason => {
+            editorEvents.serverStopped.fire(serverStoppedReason)
+        },
+        changedCursorLocation: async loc => editorEvents.changedCursorLocation.fire(loc),
+        changedInfoviewConfig: async conf => editorEvents.changedInfoviewConfig.fire(conf),
+        requestedAction: async action => editorEvents.requestedAction.fire(action),
+        // See https://rollupjs.org/guide/en/#avoiding-eval
+        // eslint-disable-next-line @typescript-eslint/no-implied-eval
+        runTestScript: async script => new Function(script)(),
+        getInfoviewHtml: async () => document.body.innerHTML,
+    };
+
+    const ec = new EditorConnection(editorApi, editorEvents);
+
+    editorEvents.initialize.on((loc: Location) => ec.events.changedCursorLocation.fire(loc))
+
+    const root = ReactDOM.createRoot(uiElement)
+    root.render(<React.StrictMode>
+        <EditorContext.Provider value={ec}>
+            <Main/>
+        </EditorContext.Provider>
+    </React.StrictMode>)
 
     setEditor(editor)
     setInfoProvider(infoProvider)

client/src/components/infoview/main.tsx

@@ -1,7 +1,6 @@
 /* Partly copied from https://github.com/leanprover/vscode-lean4/blob/master/lean4-infoview/src/infoview/main.tsx */
 
 import * as React from 'react';
-import * as ReactDOM from 'react-dom/client';
 import type { DidCloseTextDocumentParams, Location, DocumentUri } from 'vscode-languageserver-protocol';
 
 import 'tachyons/css/tachyons.css';
@@ -17,12 +16,10 @@ import { AllMessages, WithLspDiagnosticsContext } from './messages';
 import { useClientNotificationEffect, useEventResult, useServerNotificationState } from '../../../../node_modules/lean4-infoview/src/infoview/util';
 import { EditorContext, ConfigContext, ProgressContext, VersionContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts';
 import { WithRpcSessions } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions';
-import { EditorConnection, EditorEvents } from '../../../../node_modules/lean4-infoview/src/infoview/editorConnection';
-import { EventEmitter } from '../../../../node_modules/lean4-infoview/src/infoview/event';
 import { ServerVersion } from '../../../../node_modules/lean4-infoview/src/infoview/serverVersion';
 
 
-function Main(props: {}) {
+export function Main(props: {}) {
     const ec = React.useContext(EditorContext);
 
     /* Set up updates to the global infoview state on editor events. */
@@ -85,59 +82,3 @@ function Main(props: {}) {
     </ConfigContext.Provider>
     );
 }
-
-/**
-  * Render the Lean infoview into the DOM element `uiElement`.
-  *
-  * @param editorApi is a collection of methods which the infoview needs to be able to invoke
-  * on the editor in order to function correctly (such as inserting text or moving the cursor).
-  * @returns a collection of methods which must be invoked when the relevant editor events occur.
-  */
-export function renderInfoview(editorApi: EditorApi, uiElement: HTMLElement): InfoviewApi {
-    const editorEvents: EditorEvents = {
-        initialize: new EventEmitter(),
-        gotServerNotification: new EventEmitter(),
-        sentClientNotification: new EventEmitter(),
-        serverRestarted: new EventEmitter(),
-        serverStopped: new EventEmitter(),
-        changedCursorLocation: new EventEmitter(),
-        changedInfoviewConfig: new EventEmitter(),
-        runTestScript: new EventEmitter(),
-        requestedAction: new EventEmitter(),
-    };
-
-    // Challenge: write a type-correct fn from `Eventify<T>` to `T` without using `any`
-    const infoviewApi: InfoviewApi = {
-        initialize: async l => editorEvents.initialize.fire(l),
-        gotServerNotification: async (method, params) => {
-            editorEvents.gotServerNotification.fire([method, params]);
-        },
-        sentClientNotification: async (method, params) => {
-            editorEvents.sentClientNotification.fire([method, params]);
-        },
-        serverRestarted: async r => editorEvents.serverRestarted.fire(r),
-        serverStopped: async serverStoppedReason => {
-            editorEvents.serverStopped.fire(serverStoppedReason)
-        },
-        changedCursorLocation: async loc => editorEvents.changedCursorLocation.fire(loc),
-        changedInfoviewConfig: async conf => editorEvents.changedInfoviewConfig.fire(conf),
-        requestedAction: async action => editorEvents.requestedAction.fire(action),
-        // See https://rollupjs.org/guide/en/#avoiding-eval
-        // eslint-disable-next-line @typescript-eslint/no-implied-eval
-        runTestScript: async script => new Function(script)(),
-        getInfoviewHtml: async () => document.body.innerHTML,
-    };
-
-    const ec = new EditorConnection(editorApi, editorEvents);
-
-    editorEvents.initialize.on((loc: Location) => ec.events.changedCursorLocation.fire(loc))
-
-    const root = ReactDOM.createRoot(uiElement)
-    root.render(<React.StrictMode>
-        <EditorContext.Provider value={ec}>
-            <Main/>
-        </EditorContext.Provider>
-    </React.StrictMode>)
-
-    return infoviewApi;
-}