phc
/
lean4game
6
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

update lean4web dependency

Browse Source
cleanup_stuff
Alexander Bentkamp 1 year ago
parent d18b48db2f
commit 6bced7575b
3 changed files with 41 additions and 36 deletions
Show Stats Download Patch File Download Diff File

31
client/src/connection.ts
Unescape Escape View File

@ -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

44
package-lock.json generated
Unescape Escape View File

@ -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",

2
package.json
Unescape Escape View File

@ -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",

Write Preview
Loading…
Cancel
Save