use webworker

client/public/lean.js

@@ -0,0 +1 @@
+/home/alex/Projects/lean4/build/release/stage1/bin/lean.js

client/public/lean.wasm

@@ -0,0 +1 @@
+/home/alex/Projects/lean4/build/release/stage1/bin/lean.wasm

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)
+})

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

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<void> {
       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)
       // );

index.html

@@ -22,102 +22,6 @@
       +49 211 81-12173<br />
     </p>
   </noscript>
-  <script>
-
-    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);
-    }};
-    </script>
-    <script src="bin/lean.js"></script>
   <script type="module" src="/client/src/index.tsx"></script>
 </body>