From 0e652256f850fe50e641062f064f8f7ab7dea72c Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Fri, 8 Dec 2023 00:51:28 +0100 Subject: [PATCH] Revert "update lean4web dependency" This reverts commit 6bced7575b335dd41b16895ab3f70a517be6297b. --- client/src/connection.ts | 31 +++------------------------- package-lock.json | 44 +++++++++++++++++++++++++++++----------- package.json | 2 +- 3 files changed, 36 insertions(+), 41 deletions(-) diff --git a/client/src/connection.ts b/client/src/connection.ts index a0d452e..3a132a8 100644 --- a/client/src/connection.ts +++ b/client/src/connection.ts @@ -3,9 +3,8 @@ */ 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 @@ -19,32 +18,8 @@ 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 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, () => {}) + const uri = monaco.Uri.parse('file:///') + this.leanClient = new LeanClient(socketUrl, undefined, uri, () => {}) } return this.leanClient diff --git a/package-lock.json b/package-lock.json index 66425b5..5f190c3 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:leanprover-community/lean4web#cleanup", + "lean4web": "github:hhu-adam/lean4web", "octokit": "^2.0.14", "path-browserify": "^1.0.1", "react": "^18.2.0", @@ -6259,11 +6259,26 @@ "integrity": "sha512-NmWvPnx0F1SfrQbYwOi7OeaNGokp9XhzNioJ/CSBs8Qa4vxug81mhJEAVZwxXuBmYB5KDRfMq/F3RR0BIU7sWg==" }, "node_modules/axios": { - "version": "0.24.0", - "resolved": "https://registry.npmjs.org/axios/-/axios-0.24.0.tgz", - "integrity": "sha512-Q6cWsys88HoPgAaFAVUb0WpPk0O8iTeisR9IMqy9G8AbO4NlpVknrnQS03zzF9PGAWgO3cgletO3VjV/P7VztA==", + "version": "1.6.2", + "resolved": "https://registry.npmjs.org/axios/-/axios-1.6.2.tgz", + "integrity": "sha512-7i24Ri4pmDRfJTR7LDBhsOTtcm+9kjX5WiY1X3wIisx6G9So3pfMkEiU7emUBe46oceVImccTEM3k6C5dbVW8A==", "dependencies": { - "follow-redirects": "^1.14.4" + "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" } }, "node_modules/babel-core": { @@ -10423,14 +10438,14 @@ } }, "node_modules/lean4": { - "version": "0.0.118", - "resolved": "https://gitpkg.now.sh/leanprover/vscode-lean4/vscode-lean4?3f62c2a45d2e1861cdb448673a271d03d915902a", - "integrity": "sha512-O+mQy8Zq3AdmEVcJP/DHjUwUmOFenLGonamgO+aL8uWOEenFi2WEgyD/PvvOucHzTsEOOaJly5YGJgoYXOCA0w==", + "version": "0.0.119", + "resolved": "https://gitpkg.now.sh/leanprover/vscode-lean4/vscode-lean4?8d0cc34dcfa00da8b4a48394ba1fb3a600e3f985", + "integrity": "sha512-hA7bb0EFlNwtk7+/7gO5OZS7HtrhmoRacE/b2etFBYG4FbkZd/NKTcs5PHGcKsYXeVghkOOZjw0uhNWaeW3gvw==", "license": "Apache-2.0", "dependencies": { "@leanprover/infoview": "~0.4.3", "@leanprover/infoview-api": "~0.2.1", - "axios": "~0.24.0", + "axios": "^1.6.2", "cheerio": "^1.0.0-rc.10", "mobx": "5.15.7", "semver": "^7.5.4", @@ -10498,7 +10513,7 @@ }, "node_modules/lean4web": { "version": "0.1.0", - "resolved": "git+ssh://git@github.com/leanprover-community/lean4web.git#53746f9f000ff6d92dcab8bdc526cebb73b76763", + "resolved": "git+ssh://git@github.com/hhu-adam/lean4web.git#6fc9c11179934cce7ca1f78140c57b6931186b42", "dependencies": { "@emotion/react": "^11.11.1", "@emotion/styled": "^11.11.0", @@ -10507,13 +10522,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.1", + "@leanprover/infoview": "^0.4.3", "@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?3f62c2a45d2e1861cdb448673a271d03d915902a", + "lean4": "https://gitpkg.now.sh/leanprover/vscode-lean4/vscode-lean4?8d0cc34dcfa00da8b4a48394ba1fb3a600e3f985", "mobx": "^6.6.2", "moment-timezone": "^0.5.39", "monaco-editor": "^0.34.1", @@ -13564,6 +13579,11 @@ "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 441ed58..d81a59c 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:leanprover-community/lean4web#cleanup", + "lean4web": "github:hhu-adam/lean4web", "octokit": "^2.0.14", "path-browserify": "^1.0.1", "react": "^18.2.0",