import the lean4 infoview so that we can modify it

2023-01-20 15:49:17 +01:00
parent 5ff9e5e26c
commit cdb2b64385
5 changed files with 171 additions and 29 deletions
@@ -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';
@@ -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<DocumentUri, LeanFileProgressProcessingInfo[]>(),
+        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 = <p>Waiting for Lean server to start...</p>
+    } else if (serverStoppedResult){
+        ret = <div><p>{serverStoppedResult.message}</p><p className="error">{serverStoppedResult.reason}</p></div>
+    } else {
+        ret = <div className="ma1">
+            <Infos />
+            {/* {curUri && <div className="mv2">
+                <AllMessages uri={curUri} />
+            </div>} */}
+        </div>
+    }
+
+    return (
+    <ConfigContext.Provider value={config}>
+        <VersionContext.Provider value={serverVersion}>
+            <WithRpcSessions>
+                <WithLspDiagnosticsContext>
+                    <ProgressContext.Provider value={allProgress}>
+                        {ret}
+                    </ProgressContext.Provider>
+                </WithLspDiagnosticsContext>
+            </WithRpcSessions>
+        </VersionContext.Provider>
+    </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;
+}
@@ -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",
@@ -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",
@@ -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/]
  };
 }