editor works basically

client/public/index.html

@@ -24,6 +24,102 @@
       </a>
     </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 src="bundle.js"></script>
 </body>
 

client/src/editor/leanclient.ts

@@ -20,7 +20,7 @@ import {
   State
 } from 'monaco-languageclient'
 import * as ls from 'vscode-languageserver-protocol'
-import { toSocket, WebSocketMessageReader, WebSocketMessageWriter } from 'vscode-ws-jsonrpc'
+import { toSocket } from 'vscode-ws-jsonrpc'
 
 import {
   // toolchainPath, lakePath, addServerEnvPaths, serverArgs, serverLoggingEnabled, serverLoggingPath, shouldAutofocusOutput,
@@ -39,6 +39,7 @@ import { join } from 'path'
 import { SemVer } from 'semver'
 // import { fileExists, isFileInFolder } from './utils/fsHelper'
 import { c2pConverter, p2cConverter, patchConverters } from './utils/converters'
+import { WasmReader, WasmWriter, WebSocketMessageWriter, WebSocketMessageReader } from '../wasm'
 
 const escapeRegExp = (s: string) => s.replace(/[.*+?^${}()|[\]\\]/g, '\\$&')
 
@@ -104,7 +105,7 @@ export class LeanClient implements Disposable {
   constructor (private readonly socketUrl: string, workspaceFolder: WorkspaceFolder | undefined, folderUri: Uri,
     public readonly showRestartMessage: () => void) {
     // this.storageManager = storageManager
-    // this.outputChannel = outputChannel
+    // this.outputChannel WebSocketMessageWriter= outputChannel
     this.workspaceFolder = workspaceFolder // can be null when opening adhoc files.
     this.folderUri = folderUri
     // this.elanDefaultToolchain = elanDefaultToolchain
@@ -323,8 +324,8 @@ export class LeanClient implements Disposable {
               })
               websocket.addEventListener('open', () => {
                 const socket = toSocket(websocket)
-                const reader = new WebSocketMessageReader(socket)
-                const writer = new WebSocketMessageWriter(socket)
+                const reader = new WasmReader()
+                const writer = new WasmWriter()
                 resolve({
                   reader,
                   writer

client/src/index.tsx

@@ -5,4 +5,4 @@ import App from './App';
 
 const container = document.getElementById('root');
 const root = createRoot(container!);
-root.render(<React.StrictMode><App /></React.StrictMode>);
+root.render(<App />);