diff --git a/client/src/app.tsx b/client/src/app.tsx index 4dda0fd..3521e2f 100644 --- a/client/src/app.tsx +++ b/client/src/app.tsx @@ -37,10 +37,6 @@ function App() { } }, [lockMobile]) - React.useEffect(() => { - connection.startLeanClient(gameId); - }, [gameId]) - return (
diff --git a/client/src/components/level.tsx b/client/src/components/level.tsx index 3b6653d..4aa3daa 100644 --- a/client/src/components/level.tsx +++ b/client/src/components/level.tsx @@ -18,7 +18,6 @@ import { EditorConnection, EditorEvents } from '../../../node_modules/lean4-info import { EventEmitter } from '../../../node_modules/lean4-infoview/src/infoview/event' import { GameIdContext } from '../app' -import { ConnectionContext, connection, useLeanClient } from '../connection' import { useAppDispatch, useAppSelector } from '../hooks' import { useGetGameInfoQuery, useLoadInventoryOverviewQuery, useLoadLevelQuery } from '../state/api' import { changedSelection, codeEdited, selectCode, selectSelections, selectCompleted, helpEdited, @@ -44,6 +43,15 @@ import 'lean4web/client/src/editor/infoview.css' import 'lean4web/client/src/editor/vscode.css' import '../css/level.css' import { LevelAppBar } from './app_bar' +import { LeanClient } from 'lean4web/client/src/editor/leanclient' +import { DisposingWebSocketMessageReader } from 'lean4web/client/src/reader' +import { WebSocketMessageWriter, toSocket } from 'vscode-ws-jsonrpc' +import { IConnectionProvider } from 'monaco-languageclient' +import { monacoSetup } from 'lean4web/client/src/monacoSetup' +import { onigasmH } from 'onigasm/lib/onigasmH' + + +monacoSetup() function Level() { const params = useParams() @@ -293,11 +301,11 @@ function PlayableLevel({impressum, setImpressum}) { // a hint at the beginning of the proof... const [selectedStep, setSelectedStep] = useState() - // if the user inventory changes, notify the server - useEffect(() => { - let leanClient = connection.getLeanClient(gameId) - leanClient.sendNotification('$/game/setInventory', {inventory: inventory, difficulty: difficulty}) - }, [inventory]) + // TODO: if the user inventory changes, notify the server + // useEffect(() => { + // let leanClient = connection.getLeanClient(gameId) + // leanClient.sendNotification('$/game/setInventory', {inventory: inventory, difficulty: difficulty}) + // }, [inventory]) useEffect (() => { // Lock editor mode @@ -372,7 +380,7 @@ function PlayableLevel({impressum, setImpressum}) { // Effect when command line mode gets enabled useEffect(() => { - if (editor && typewriterMode) { + if (onigasmH && editor && typewriterMode) { let code = editor.getModel().getLinesContent().filter(line => line.trim()) editor.executeEdits("typewriter", [{ range: editor.getModel().getFullModelRange(), @@ -395,7 +403,7 @@ function PlayableLevel({impressum, setImpressum}) { // editor.setSelection(monaco.Selection.fromPositions(endPos, endPos)) // } } - }, [editor, typewriterMode]) + }, [editor, typewriterMode, onigasmH == null]) return <>
@@ -531,21 +539,29 @@ function Introduction({impressum, setImpressum}) { function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChangeContent, onDidChangeSelection) { - const connection = React.useContext(ConnectionContext) const gameId = React.useContext(GameIdContext) const {worldId, levelId} = useContext(WorldLevelIdContext) - const [editor, setEditor] = useState(null) const [infoProvider, setInfoProvider] = useState(null) - const [infoviewApi, setInfoviewApi] = useState(null) const [editorConnection, setEditorConnection] = useState(null) - // Create Editor + const uriStr = `file:///${worldId}/${levelId}` + const uri = monaco.Uri.parse(uriStr) + useEffect(() => { + const model = monaco.editor.createModel(initialCode ?? '', 'lean4', uri) + if (onDidChangeContent) { + model.onDidChangeContent(() => onDidChangeContent(model.getValue())) + } + const editor = monaco.editor.create(codeviewRef.current!, { + model, glyphMargin: true, quickSuggestions: false, + lineDecorationsWidth: 5, + folding: false, + lineNumbers: 'on', lightbulb: { enabled: true }, @@ -557,11 +573,61 @@ function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChange enabled: false }, lineNumbersMinChars: 3, + tabSize: 2, 'semanticHighlighting.enabled': true, theme: 'vs-code-theme-converted' }) + if (onDidChangeSelection) { + editor.onDidChangeCursorSelection(() => onDidChangeSelection(editor.getSelections())) + } + if (initialSelections) { + console.debug("Initial Selection: ", initialSelections) + // BUG: Somehow I get an `invalid arguments` bug here + // editor.setSelections(initialSelections) + } + setEditor(editor) + const abbrevRewriter = new AbbreviationRewriter(new AbbreviationProvider(), model, editor) + + const socketUrl = ((window.location.protocol === "https:") ? "wss://" : "ws://") + window.location.host + '/websocket/' + gameId + + const connectionProvider : IConnectionProvider = { + get: async () => { + return await new Promise((resolve, reject) => { + console.log(`connecting ${socketUrl}`) + const websocket = new WebSocket(socketUrl) + websocket.addEventListener('error', (ev) => { + reject(ev) + }) + websocket.addEventListener('message', (msg) => { + // console.log(msg.data) + }) + websocket.addEventListener('open', () => { + const socket = toSocket(websocket) + const reader = new DisposingWebSocketMessageReader(socket) + const writer = new WebSocketMessageWriter(socket) + resolve({ + reader, + writer + }) + }) + }) + } + } - const infoProvider = new InfoProvider(connection.getLeanClient(gameId)) + // Following `vscode-lean4/webview/index.ts` + const client = new LeanClient(connectionProvider, showRestartMessage) + const infoProvider = new InfoProvider(client) + // const div: HTMLElement = infoviewRef.current! + const imports = { + '@leanprover/infoview': `${window.location.origin}/index.production.min.js`, + 'react': `${window.location.origin}/react.production.min.js`, + 'react/jsx-runtime': `${window.location.origin}/react-jsx-runtime.production.min.js`, + 'react-dom': `${window.location.origin}/react-dom.production.min.js`, + 'react-popper': `${window.location.origin}/react-popper.production.min.js` + } + // loadRenderInfoview(imports, [infoProvider.getApi(), div], setInfoviewApi) + setInfoProvider(infoProvider) + client.restart() const editorApi = infoProvider.getApi() @@ -606,54 +672,27 @@ function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChange setEditor(editor) setInfoProvider(infoProvider) - setInfoviewApi(infoviewApi) - return () => { infoProvider.dispose(); editor.dispose() } - }, []) + infoProvider.openPreview(editor, infoviewApi) + const taskgutter = new LeanTaskGutter(infoProvider.client, editor) - const {leanClient, leanClientStarted} = useLeanClient(gameId) - const uriStr = `file:///${worldId}/${levelId}` - const uri = monaco.Uri.parse(uriStr) - - // Create model when level changes - useEffect(() => { - if (editor && leanClientStarted) { - - let model = monaco.editor.getModel(uri) - if (!model) { - model = monaco.editor.createModel(initialCode, 'lean4', uri) - } - model.onDidChangeContent(() => onDidChangeContent(model.getValue())) - editor.onDidChangeCursorSelection(() => onDidChangeSelection(editor.getSelections())) - editor.setModel(model) - if (initialSelections) { - console.debug("Initial Selection: ", initialSelections) - // BUG: Somehow I get an `invalid arguments` bug here - // editor.setSelections(initialSelections) - } + // TODO: + // setRestart(() => restart) - return () => { - editorConnection.api.sendClientNotification(uriStr, "textDocument/didClose", {textDocument: {uri: uriStr}}) - model.dispose(); - } + return () => { + editor.dispose(); + model.dispose(); + abbrevRewriter.dispose(); + taskgutter.dispose(); + infoProvider.dispose(); + client.dispose(); } - }, [editor, levelId, connection, leanClientStarted]) - - - useEffect(() => { - if (editor && leanClientStarted) { - - let model = monaco.editor.getModel(uri) - infoviewApi.serverRestarted(leanClient.initializeResult) - - infoProvider.openPreview(editor, infoviewApi) - - const taskGutter = new LeanTaskGutter(infoProvider.client, editor) - const abbrevRewriter = new AbbreviationRewriter(new AbbreviationProvider(), model, editor) + }, [gameId, worldId, levelId]) - return () => { abbrevRewriter.dispose(); taskGutter.dispose(); } - } - }, [editor, connection, leanClientStarted]) + const showRestartMessage = () => { + // setRestartMessage(true) + console.log("TODO: SHOW RESTART MESSAGE") + } return {editor, infoProvider, editorConnection} } diff --git a/client/src/connection.ts b/client/src/connection.ts deleted file mode 100644 index 3a132a8..0000000 --- a/client/src/connection.ts +++ /dev/null @@ -1,68 +0,0 @@ -/** - * @fileOverview todo - */ - -import * as React from 'react'; -import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js' -import { LeanClient } from 'lean4web/client/src/editor/leanclient'; - -export class Connection { - private game: string = undefined // We only keep a connection to a single game at a time - private leanClient: LeanClient = null - - getLeanClient(game): LeanClient { - if (this.game !== game) { - if (this.leanClient) { - this.leanClient.stop() // Stop previous Lean client - } - this.game = game - // Start a new Lean client for the new `gameId`. - const socketUrl = ((window.location.protocol === "https:") ? "wss://" : "ws://") + window.location.host + '/websocket/' + game - const uri = monaco.Uri.parse('file:///') - this.leanClient = new LeanClient(socketUrl, undefined, uri, () => {}) - } - - return this.leanClient - } - - /** If not already started, starts the Lean client. resolves the returned promise as soon as a - * Lean client is running. - */ - startLeanClient = (game) => { - return new Promise((resolve) => { - const leanClient = this.getLeanClient(game) - if (leanClient.isRunning()) { - resolve(leanClient) - } else { - if (!leanClient.isStarted()) { - leanClient.start() - } - leanClient.restarted(() => { - // This keep alive message is not recognized by the server, - // but it makes sure that the websocket connection does not - // time out after 60 seconds. - setInterval(() => {leanClient.sendNotification('$/keepAlive', {}) }, 5000) - resolve(leanClient) - }) - } - }) - } -} - -export const connection = new Connection() - -export const ConnectionContext = React.createContext(null); - -export const useLeanClient = (gameId) => { - const leanClient = connection.getLeanClient(gameId) - const [leanClientStarted, setLeanClientStarted] = React.useState(leanClient.isStarted()) - - React.useEffect(() => { - const t1 = leanClient.restarted(() => { console.log("START"); setLeanClientStarted(true) }) - const t2 = leanClient.stopped(() => { console.log("STOP"); setLeanClientStarted(false) }) - - return () => {t1.dispose(); t2.dispose()} - }, [leanClient, setLeanClientStarted]) - - return {leanClientStarted, leanClient} -} diff --git a/client/src/index.tsx b/client/src/index.tsx index c42b6dc..5fff511 100644 --- a/client/src/index.tsx +++ b/client/src/index.tsx @@ -1,7 +1,6 @@ import * as React from 'react' import { createRoot } from 'react-dom/client' import App from './app' -import { ConnectionContext, connection } from './connection' import { store } from './state/store' import { Provider } from 'react-redux' import type { RouteObject } from "react-router" @@ -10,11 +9,8 @@ import ErrorPage from './components/error_page' import Welcome from './components/welcome' import LandingPage from './components/landing_page' import Level from './components/level' -import { monacoSetup } from 'lean4web/client/src/monacoSetup' -monacoSetup() - // If `VITE_LEAN4GAME_SINGLE` is set to true, then `/` should be redirected to // `/g/local/game`. This is used for the devcontainer setup @@ -61,9 +57,7 @@ const root = createRoot(container!); root.render( - - - + ); diff --git a/client/src/state/store.ts b/client/src/state/store.ts index a2294de..4406c84 100644 --- a/client/src/state/store.ts +++ b/client/src/state/store.ts @@ -19,11 +19,7 @@ export const store = configureStore({ }, // Make connection available in thunks: middleware: getDefaultMiddleware => - getDefaultMiddleware({ - thunk: { - extraArgument: { connection } - } - }).concat(apiSlice.middleware), + getDefaultMiddleware().concat(apiSlice.middleware), }); /** diff --git a/package-lock.json b/package-lock.json index 0d8025f..c985568 100644 --- a/package-lock.json +++ b/package-lock.json @@ -31,7 +31,7 @@ "debounce": "^1.2.1", "express": "^4.18.2", "lean4-infoview": "https://gitpkg.now.sh/leanprover/vscode-lean4/lean4-infoview?de0062c", - "lean4web": "github:hhu-adam/lean4web", + "lean4web": "github:hhu-adam/lean4web#03fe27835115d6b00c02e3f61cefd4a1ba9e3ae0", "octokit": "^2.0.14", "path-browserify": "^1.0.1", "react": "^18.2.0", @@ -2539,9 +2539,9 @@ } }, "node_modules/@leanprover/infoview": { - "version": "0.4.3", - "resolved": "https://registry.npmjs.org/@leanprover/infoview/-/infoview-0.4.3.tgz", - "integrity": "sha512-SufdOr2myHAbZNUmobfQdAhsEC5H9ddi3KS0z1v/8riWSMm+yJk3u4LxVuzCmmSmV2QxFqtFzn5z+HQqj1Vo7g==", + "version": "0.4.4", + "resolved": "https://registry.npmjs.org/@leanprover/infoview/-/infoview-0.4.4.tgz", + "integrity": "sha512-OxHffFaHcEudLyBEWpicOl7TfXuTYxW5Sz1RkHdUINWJpQsQn60YDF5fNRKmSb0d/fm7p+LVeBvM273jvfR5wQ==", "dependencies": { "@leanprover/infoview-api": "~0.2.1", "@vscode/codicons": "^0.0.32", @@ -10081,7 +10081,8 @@ }, "node_modules/lean4web": { "version": "0.1.0", - "resolved": "git+ssh://git@github.com/hhu-adam/lean4web.git#6fc9c11179934cce7ca1f78140c57b6931186b42", + "resolved": "git+ssh://git@github.com/hhu-adam/lean4web.git#03fe27835115d6b00c02e3f61cefd4a1ba9e3ae0", + "integrity": "sha512-VwKtgF6CUQtC3616+/y4I4DURdaVNU7Bvs++tDbL39YDOSomjLyauLZzzyXRr8/CAFGsnaF13eiafENWMzZE5Q==", "dependencies": { "@emotion/react": "^11.11.1", "@emotion/styled": "^11.11.0", @@ -10090,7 +10091,7 @@ "@fortawesome/fontawesome-svg-core": "^6.2.0", "@fortawesome/free-solid-svg-icons": "^6.2.0", "@fortawesome/react-fontawesome": "^0.2.0", - "@leanprover/infoview": "^0.4.3", + "@leanprover/infoview": "^0.4.4", "@mui/material": "^5.13.7", "@vitejs/plugin-react-swc": "^3.4.0", "express": "^4.18.2", diff --git a/package.json b/package.json index d0d6793..d461744 100644 --- a/package.json +++ b/package.json @@ -28,7 +28,7 @@ "debounce": "^1.2.1", "express": "^4.18.2", "lean4-infoview": "https://gitpkg.now.sh/leanprover/vscode-lean4/lean4-infoview?de0062c", - "lean4web": "github:hhu-adam/lean4web", + "lean4web": "github:hhu-adam/lean4web#03fe27835115d6b00c02e3f61cefd4a1ba9e3ae0", "octokit": "^2.0.14", "path-browserify": "^1.0.1", "react": "^18.2.0",