diff --git a/client/src/components/Level.tsx b/client/src/components/Level.tsx index aa3cf78..35e02f1 100644 --- a/client/src/components/Level.tsx +++ b/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` 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( + +
+ + ) setEditor(editor) setInfoProvider(infoProvider) diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx index 0623b3f..4728820 100644 --- a/client/src/components/infoview/main.tsx +++ b/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: {}) { ); } - -/** - * 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` 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( - -
- - ) - - return infoviewApi; -}