Skip to content

Commit

Permalink
update lean4web dependency
Browse files Browse the repository at this point in the history
  • Loading branch information
abentkamp committed Dec 1, 2023
1 parent d18b48d commit 6bced75
Show file tree
Hide file tree
Showing 3 changed files with 41 additions and 36 deletions.
31 changes: 28 additions & 3 deletions client/src/connection.ts
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down
44 changes: 12 additions & 32 deletions package-lock.json

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion package.json
Original file line number Diff line number Diff line change
Expand Up @@ -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",
Expand Down

0 comments on commit 6bced75

Please sign in to comment.