diff --git a/client/src/connection.ts b/client/src/connection.ts index 3a132a83..a0d452e1 100644 --- a/client/src/connection.ts +++ b/client/src/connection.ts @@ -3,8 +3,9 @@ */ 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'; +import { IConnectionProvider } from 'monaco-languageclient' +import { toSocket, WebSocketMessageReader, WebSocketMessageWriter } from 'vscode-ws-jsonrpc' export class Connection { private game: string = undefined // We only keep a connection to a single game at a time @@ -18,8 +19,32 @@ export class Connection { 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, () => {}) + + 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 WebSocketMessageReader(socket) + const writer = new WebSocketMessageWriter(socket) + resolve({ + reader, + writer + }) + }) + }) + } + } + + this.leanClient = new LeanClient(connectionProvider, () => {}) } return this.leanClient diff --git a/package-lock.json b/package-lock.json index 5f190c33..66425b54 100644 --- a/package-lock.json +++ b/package-lock.json @@ -27,7 +27,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:leanprover-community/lean4web#cleanup", "octokit": "^2.0.14", "path-browserify": "^1.0.1", "react": "^18.2.0", @@ -6259,26 +6259,11 @@ "integrity": "sha512-NmWvPnx0F1SfrQbYwOi7OeaNGokp9XhzNioJ/CSBs8Qa4vxug81mhJEAVZwxXuBmYB5KDRfMq/F3RR0BIU7sWg==" }, "node_modules/axios": { - "version": "1.6.2", - "resolved": "https://registry.npmjs.org/axios/-/axios-1.6.2.tgz", - "integrity": "sha512-7i24Ri4pmDRfJTR7LDBhsOTtcm+9kjX5WiY1X3wIisx6G9So3pfMkEiU7emUBe46oceVImccTEM3k6C5dbVW8A==", + "version": "0.24.0", + "resolved": "https://registry.npmjs.org/axios/-/axios-0.24.0.tgz", + "integrity": "sha512-Q6cWsys88HoPgAaFAVUb0WpPk0O8iTeisR9IMqy9G8AbO4NlpVknrnQS03zzF9PGAWgO3cgletO3VjV/P7VztA==", "dependencies": { - "follow-redirects": "^1.15.0", - "form-data": "^4.0.0", - "proxy-from-env": "^1.1.0" - } - }, - "node_modules/axios/node_modules/form-data": { - "version": "4.0.0", - "resolved": "https://registry.npmjs.org/form-data/-/form-data-4.0.0.tgz", - "integrity": "sha512-ETEklSGi5t0QMZuiXoA/Q6vcnxcLQP5vdugSpuAyi6SVGi2clPPp+xgEhuMaHC+zGgn31Kd235W35f7Hykkaww==", - "dependencies": { - "asynckit": "^0.4.0", - "combined-stream": "^1.0.8", - "mime-types": "^2.1.12" - }, - "engines": { - "node": ">= 6" + "follow-redirects": "^1.14.4" } }, "node_modules/babel-core": { @@ -10438,14 +10423,14 @@ } }, "node_modules/lean4": { - "version": "0.0.119", - "resolved": "https://gitpkg.now.sh/leanprover/vscode-lean4/vscode-lean4?8d0cc34dcfa00da8b4a48394ba1fb3a600e3f985", - "integrity": "sha512-hA7bb0EFlNwtk7+/7gO5OZS7HtrhmoRacE/b2etFBYG4FbkZd/NKTcs5PHGcKsYXeVghkOOZjw0uhNWaeW3gvw==", + "version": "0.0.118", + "resolved": "https://gitpkg.now.sh/leanprover/vscode-lean4/vscode-lean4?3f62c2a45d2e1861cdb448673a271d03d915902a", + "integrity": "sha512-O+mQy8Zq3AdmEVcJP/DHjUwUmOFenLGonamgO+aL8uWOEenFi2WEgyD/PvvOucHzTsEOOaJly5YGJgoYXOCA0w==", "license": "Apache-2.0", "dependencies": { "@leanprover/infoview": "~0.4.3", "@leanprover/infoview-api": "~0.2.1", - "axios": "^1.6.2", + "axios": "~0.24.0", "cheerio": "^1.0.0-rc.10", "mobx": "5.15.7", "semver": "^7.5.4", @@ -10513,7 +10498,7 @@ }, "node_modules/lean4web": { "version": "0.1.0", - "resolved": "git+ssh://git@github.com/hhu-adam/lean4web.git#6fc9c11179934cce7ca1f78140c57b6931186b42", + "resolved": "git+ssh://git@github.com/leanprover-community/lean4web.git#53746f9f000ff6d92dcab8bdc526cebb73b76763", "dependencies": { "@emotion/react": "^11.11.1", "@emotion/styled": "^11.11.0", @@ -10522,13 +10507,13 @@ "@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.1", "@mui/material": "^5.13.7", "@vitejs/plugin-react-swc": "^3.4.0", "express": "^4.18.2", "file-saver": "^2.0.5", "ip-anonymize": "^0.1.0", - "lean4": "https://gitpkg.now.sh/leanprover/vscode-lean4/vscode-lean4?8d0cc34dcfa00da8b4a48394ba1fb3a600e3f985", + "lean4": "https://gitpkg.now.sh/leanprover/vscode-lean4/vscode-lean4?3f62c2a45d2e1861cdb448673a271d03d915902a", "mobx": "^6.6.2", "moment-timezone": "^0.5.39", "monaco-editor": "^0.34.1", @@ -13579,11 +13564,6 @@ "node": ">= 0.10" } }, - "node_modules/proxy-from-env": { - "version": "1.1.0", - "resolved": "https://registry.npmjs.org/proxy-from-env/-/proxy-from-env-1.1.0.tgz", - "integrity": "sha512-D+zkORCbA9f1tdWRK0RaCR3GPv50cMxcrz4X8k5LTSUD1Dkw47mKJEZQNunItRTkWwgtaUSo1RVFRIG9ZXiFYg==" - }, "node_modules/psl": { "version": "1.9.0", "resolved": "https://registry.npmjs.org/psl/-/psl-1.9.0.tgz", diff --git a/package.json b/package.json index d81a59ca..441ed583 100644 --- a/package.json +++ b/package.json @@ -24,7 +24,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:leanprover-community/lean4web#cleanup", "octokit": "^2.0.14", "path-browserify": "^1.0.1", "react": "^18.2.0",