From 32e5348ce56c265b0bfe9a98f18e4ca814c414c5 Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Fri, 3 Nov 2023 18:07:54 +0100 Subject: [PATCH] use webworker --- client/public/bin | 1 - client/public/lean.js | 1 + client/public/lean.wasm | 1 + client/public/worker.js | 103 ++++++++++++++++++++++++++++++++ client/src/editor/leanclient.ts | 5 +- client/src/wasm.ts | 12 ++-- index.html | 96 ----------------------------- 7 files changed, 114 insertions(+), 105 deletions(-) delete mode 120000 client/public/bin create mode 120000 client/public/lean.js create mode 120000 client/public/lean.wasm create mode 100644 client/public/worker.js diff --git a/client/public/bin b/client/public/bin deleted file mode 120000 index aeb71b92..00000000 --- a/client/public/bin +++ /dev/null @@ -1 +0,0 @@ -/home/alex/Projects/lean4/build/release/stage1/bin \ No newline at end of file diff --git a/client/public/lean.js b/client/public/lean.js new file mode 120000 index 00000000..58f83aad --- /dev/null +++ b/client/public/lean.js @@ -0,0 +1 @@ +/home/alex/Projects/lean4/build/release/stage1/bin/lean.js \ No newline at end of file diff --git a/client/public/lean.wasm b/client/public/lean.wasm new file mode 120000 index 00000000..fa52e278 --- /dev/null +++ b/client/public/lean.wasm @@ -0,0 +1 @@ +/home/alex/Projects/lean4/build/release/stage1/bin/lean.wasm \ No newline at end of file diff --git a/client/public/worker.js b/client/public/worker.js new file mode 100644 index 00000000..0591d705 --- /dev/null +++ b/client/public/worker.js @@ -0,0 +1,103 @@ + +const IO = { + _resolveGetLine: null, + _resolveRead: null, + _readPointer: null, + _nbytes: 0, + bufferStdIn : "", + putStrListeners: [], + listenPutStr(callback) { + this.putStrListeners.push(callback) + }, + putStr(str) { + console.log('PUTSTR' + str) + str = str.split('\n')[2] + this.putStrListeners.forEach((listener) => { + listener(str) + }) + }, + async getLine() { + return new Promise((resolve, reject) => { + this._resolveGetLine = resolve + this.flushStdIn(); + }); + }, + async read(ptr, nbytes) { + this._nbytes = nbytes + this._readPointer = ptr + return new Promise((resolve, reject) => { + this._resolveRead = resolve + this.flushStdIn(); + }); + }, + flushStdIn() { + if(this._resolveGetLine) { + var lineBreak = this.bufferStdIn.indexOf("\n") + if (lineBreak != -1) { + this._resolveGetLine(stringToNewUTF8(this.bufferStdIn.substring(0,lineBreak+1))) + this.bufferStdIn = this.bufferStdIn.substring(lineBreak+1) + this._resolveGetLine = null + } + } + if(this._resolveRead) { + // console.log(`read: ${this.bufferStdIn}`) + stringToUTF8(this.bufferStdIn, this._readPointer, this._nbytes); + this._resolveRead() + this.bufferStdIn = "" + this._resolveRead = null + } + }, + putLine(data) { + console.log("Client: ",data) + const str = data + '\r\n' + const byteLength = lengthBytesUTF8(str) + this.bufferStdIn += `Content-Length: ${byteLength}\r\n\r\n` + str + this.flushStdIn(); + } +} + + +var input = "" +var i = 0; + +function submit (ev) { +ev.preventDefault() +return false; +} + +var stdoutBuffer = "" +var stderrBuffer = "" + + +var Module = { + "arguments": ["--worker"], + "preRun": function() { + function stdin() { + if (i < input.length) { + i++; + return input.charCodeAt(i);// Return ASCII code of character, or null if no input + } else { + return null + } + } + + function stdout(asciiCode) { + stdoutBuffer += String.fromCharCode(asciiCode) + } + + function stderr(asciiCode) { + stderrBuffer += String.fromCharCode(asciiCode) + } + + FS.init(stdin, stdout, stderr); +}}; + +importScripts("lean.js") + +onmessage = (ev) => { + IO.putLine(ev.data) +} + +IO.listenPutStr(message => { + postMessage(message) +}) diff --git a/client/src/editor/leanclient.ts b/client/src/editor/leanclient.ts index 6b8b2718..b083127f 100644 --- a/client/src/editor/leanclient.ts +++ b/client/src/editor/leanclient.ts @@ -324,8 +324,9 @@ export class LeanClient implements Disposable { }) websocket.addEventListener('open', () => { const socket = toSocket(websocket) - const reader = new WasmReader() - const writer = new WasmWriter() + const worker = new Worker("worker.js") + const reader = new WasmReader(worker) + const writer = new WasmWriter(worker) resolve({ reader, writer diff --git a/client/src/wasm.ts b/client/src/wasm.ts index ddaac4eb..0a35104e 100644 --- a/client/src/wasm.ts +++ b/client/src/wasm.ts @@ -13,7 +13,7 @@ export class WasmWriter implements MessageWriter { protected errorCount = 0; errorEmitter closeEmitter - constructor() { + constructor(private worker: Worker) { this.errorEmitter = new Emitter() this.closeEmitter = new Emitter() } @@ -48,7 +48,7 @@ asError(error) { async write(msg: Message): Promise { try { const content = JSON.stringify(msg); - IO.putLine(content) + this.worker.postMessage(content) } catch (e) { this.errorCount++; this.fireError(e, msg, this.errorCount); @@ -62,10 +62,10 @@ export class WasmReader implements MessageReader { protected callback: DataCallback | undefined; protected readonly events: { message?: any, error?: any }[] = []; - constructor() { - IO.listenPutStr(message => { - this.readMessage(message) - }) + constructor(private worker: Worker) { + this.worker.onmessage = (ev) => { + this.readMessage(ev.data) + } // this.socket.onMessage(message => // this.readMessage(message) // ); diff --git a/index.html b/index.html index 6f7494b9..3d538b38 100644 --- a/index.html +++ b/index.html @@ -22,102 +22,6 @@ +49 211 81-12173

- -