From cdb2b64385fc10455705cd735022bd912b01aebc Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Fri, 20 Jan 2023 15:49:17 +0100 Subject: [PATCH] import the lean4 infoview so that we can modify it --- client/src/components/Level.tsx | 3 +- client/src/components/infoview/main.tsx | 142 ++++++++++++++++++++++++ package-lock.json | 37 +++--- package.json | 1 + webpack.config.js | 17 +-- 5 files changed, 171 insertions(+), 29 deletions(-) create mode 100644 client/src/components/infoview/main.tsx diff --git a/client/src/components/Level.tsx b/client/src/components/Level.tsx index cbe2c3c..3cb8b54 100644 --- a/client/src/components/Level.tsx +++ b/client/src/components/Level.tsx @@ -4,7 +4,8 @@ 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 { InfoviewApi } from '@leanprover/infoview' +import { renderInfoview } from './infoview/main' 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'; diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx new file mode 100644 index 0000000..54f62db --- /dev/null +++ b/client/src/components/infoview/main.tsx @@ -0,0 +1,142 @@ +/* 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'; +// import '@vscode/codicons/dist/codicon.ttf'; +import '@vscode/codicons/dist/codicon.css'; +import '../../../../node_modules/lean4-infoview/src/infoview/index.css'; + +import { LeanFileProgressParams, LeanFileProgressProcessingInfo, defaultInfoviewConfig, EditorApi, InfoviewApi } from '@leanprover/infoview-api'; + +import { Infos } from '../../../../node_modules/lean4-infoview/src/infoview/infos'; +import { AllMessages, WithLspDiagnosticsContext } from '../../../../node_modules/lean4-infoview/src/infoview/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: {}) { + const ec = React.useContext(EditorContext); + + /* Set up updates to the global infoview state on editor events. */ + const config = useEventResult(ec.events.changedInfoviewConfig) ?? defaultInfoviewConfig; + + const [allProgress, _1] = useServerNotificationState( + '$/lean/fileProgress', + new Map(), + async (params: LeanFileProgressParams) => (allProgress) => { + const newProgress = new Map(allProgress); + return newProgress.set(params.textDocument.uri, params.processing); + }, + [] + ); + + const curUri = useEventResult(ec.events.changedCursorLocation, loc => loc?.uri); + + useClientNotificationEffect( + 'textDocument/didClose', + (params: DidCloseTextDocumentParams) => { + if (ec.events.changedCursorLocation.current && + ec.events.changedCursorLocation.current.uri === params.textDocument.uri) { + ec.events.changedCursorLocation.fire(undefined) + } + }, + [] + ); + + const serverVersion = + useEventResult(ec.events.serverRestarted, result => new ServerVersion(result.serverInfo?.version ?? '')) + const serverStoppedResult = useEventResult(ec.events.serverStopped); + // NB: the cursor may temporarily become `undefined` when a file is closed. In this case + // it's important not to reconstruct the `WithBlah` wrappers below since they contain state + // that we want to persist. + let ret + if (!serverVersion) { + ret =

Waiting for Lean server to start...

+ } else if (serverStoppedResult){ + ret =

{serverStoppedResult.message}

{serverStoppedResult.reason}

+ } else { + ret =
+ + {/* {curUri &&
+ +
} */} +
+ } + + return ( + + + + + + {ret} + + + + + + ); +} + +/** + * 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; +} diff --git a/package-lock.json b/package-lock.json index d54cac3..fc6231b 100644 --- a/package-lock.json +++ b/package-lock.json @@ -21,6 +21,7 @@ "cytoscape-klay": "^3.1.4", "debounce": "^1.2.1", "express": "^4.18.2", + "lean4-infoview": "https://gitpkg.now.sh/leanprover/vscode-lean4/lean4-infoview?master", "lean4web": "github:hhu-adam/lean4web", "path-browserify": "^1.0.1", "react": "^18.2.0", @@ -2095,9 +2096,9 @@ } }, "node_modules/@leanprover/infoview-api": { - "version": "0.2.0", - "resolved": "https://registry.npmjs.org/@leanprover/infoview-api/-/infoview-api-0.2.0.tgz", - "integrity": "sha512-HnBCg9/ijvJmQkEAlHH5E50i5uQVqdOC2sT5KzUs+Bq7woL2dPNjeDFECudye5bvbLoy+kJ/x24n0eW5PuaF3w==" + "version": "0.2.1", + "resolved": "https://registry.npmjs.org/@leanprover/infoview-api/-/infoview-api-0.2.1.tgz", + "integrity": "sha512-4sYdwOhUsa5wfvo/ZsCbcm8fBWcrATciZq0sWfmi5NRbIyZ+c2QjTm6D9CeYPCNvz9yvD1KBp/2+hKEZ8SOHkA==" }, "node_modules/@leichtgewicht/ip-codec": { "version": "2.0.4", @@ -4919,20 +4920,6 @@ "integrity": "sha512-OO0pH2lK6a0hZnAdau5ItzHPI6pUlvI7jMVnxUQRtw4owF2wk8lOSabtGDCTP4Ggrg2MbGnWO9X8K1t4+fGMDw==", "dev": true }, - "node_modules/fsevents": { - "version": "2.3.2", - "resolved": "https://registry.npmjs.org/fsevents/-/fsevents-2.3.2.tgz", - "integrity": "sha512-xiqMQR4xAeHTuB9uWm+fFRcIOgKBMiOBP+eXiyT7jsgVCq1bkVygt00oASowB7EdtpOHaaPgKt812P9ab+DDKA==", - "dev": true, - "hasInstallScript": true, - "optional": true, - "os": [ - "darwin" - ], - "engines": { - "node": "^8.16.0 || ^10.6.0 || >=11.0.0" - } - }, "node_modules/function-bind": { "version": "1.1.1", "resolved": "https://registry.npmjs.org/function-bind/-/function-bind-1.1.1.tgz", @@ -6001,6 +5988,22 @@ "vscode": "^1.70.0" } }, + "node_modules/lean4-infoview": { + "name": "@leanprover/infoview", + "version": "0.4.2", + "resolved": "https://gitpkg.now.sh/leanprover/vscode-lean4/lean4-infoview?master", + "integrity": "sha512-fNrNu9Hte4WqGsuGOcJiifbovphjV9Cz4NJjg/AZcjL7i+JAjR1hy8J2t/p2sMHVaaY+NRKEfRcbyq+jpOI91A==", + "license": "Apache-2.0", + "dependencies": { + "@leanprover/infoview-api": "~0.2.1", + "@vscode/codicons": "^0.0.32", + "es-module-shims": "^1.6.2", + "marked": "^4.2.2", + "react-fast-compare": "^3.2.0", + "tachyons": "^4.12.0", + "vscode-languageserver-protocol": "^3.17.2" + } + }, "node_modules/lean4/node_modules/@leanprover/infoview": { "version": "0.3.0", "resolved": "https://registry.npmjs.org/@leanprover/infoview/-/infoview-0.3.0.tgz", diff --git a/package.json b/package.json index de3c1c7..2e511b9 100644 --- a/package.json +++ b/package.json @@ -8,6 +8,7 @@ "@emotion/styled": "^11.10.5", "@fontsource/roboto": "^4.5.8", "@fontsource/roboto-mono": "^4.5.8", + "lean4-infoview": "https://gitpkg.now.sh/leanprover/vscode-lean4/lean4-infoview?master", "@mui/icons-material": "^5.11.0", "@mui/material": "^5.11.1", "@reduxjs/toolkit": "^1.9.1", diff --git a/webpack.config.js b/webpack.config.js index 2d8864d..b9101e4 100644 --- a/webpack.config.js +++ b/webpack.config.js @@ -36,7 +36,7 @@ module.exports = env => { loader: 'ts-loader', options: { allowTsInNodeModules: true } }], - exclude: /node_modules(?!\/(lean4web|lean4))/, + exclude: /node_modules(?!\/(lean4web|lean4|lean4-infoview))/, // Allow .ts imports from node_modules/lean4web and node_modules/lean4 }, { @@ -82,16 +82,11 @@ module.exports = env => { } }), isDevelopment && new ReactRefreshWebpackPlugin(), - new webpack.ContextReplacementPlugin( - /\/@leanprover\/infoview\//, - (data) => { - // Webpack is not happy about the dynamically loaded widget code in the function - // `dynamicallyLoadComponent` in `infoview/userWidget.tsx`. If we want to support - // dynamically loaded widget code, we need to make sure that the files are available. - delete data.dependencies[0].critical; - return data; - }, - ), ].filter(Boolean), + + // Webpack is not happy about the dynamically loaded widget code in the function + // `dynamicallyLoadComponent` in `infoview/userWidget.tsx`. If we want to support + // dynamically loaded widget code, we need to make sure that the files are available. + ignoreWarnings: [/Critical dependency: the request of a dependency is an expression/] }; }