From 32686170b13d42083539f5740310541cb7d7e449 Mon Sep 17 00:00:00 2001
From: Jason Reed <jcreed@gmail.com>
Date: Fri, 15 Mar 2024 17:18:29 -0400
Subject: [PATCH] Make timeout actually work

---
 src/index.ts        | 14 +++++++-------
 src/twelf-worker.ts | 41 ++++++++++++++++++++++++++++-------------
 2 files changed, 35 insertions(+), 20 deletions(-)

diff --git a/src/index.ts b/src/index.ts
index c8f713d..ec94fb3 100644
--- a/src/index.ts
+++ b/src/index.ts
@@ -92,20 +92,20 @@ async function initTwelf(editor: EditorView) {
   }
 
   const workerRef: { worker: TwelfWorker | undefined } = { worker: undefined };
-  async function timeoutCallback(): Promise<void> {
-    workerRef.worker = undefined;
-    alert('twelf timed out, trying to restart twelf worker...');
-    workerRef.worker = await mkTwelfWorker(timeoutCallback);
-  }
-
   (document.getElementById('twelf-response') as HTMLTextAreaElement).value = '';
-  workerRef.worker = await mkTwelfWorker(timeoutCallback);
+  workerRef.worker = await mkTwelfWorker();
 
   async function execAndShowStatus(text: string): Promise<void> {
     if (workerRef.worker == undefined) {
       throw new Error(`twelf worker not ready yet`);
     }
     const result = await (workerRef.worker).exec(text);
+
+    if (result.status.t == 'timeout') {
+      workerRef.worker = undefined;
+      console.log('twelf timed out, trying to restart twelf worker...');
+      workerRef.worker = await mkTwelfWorker();
+    }
     showStatus(result.status);
     showErrors(result.errors);
     (document.getElementById('twelf-response') as HTMLTextAreaElement).value = result.output.join('');
diff --git a/src/twelf-worker.ts b/src/twelf-worker.ts
index ab0a35a..64c9f31 100644
--- a/src/twelf-worker.ts
+++ b/src/twelf-worker.ts
@@ -1,7 +1,7 @@
 import { TwelfExecRequest, TwelfExecResponse, TwelfResponse, WithId } from "./twelf-worker-types";
 
-export async function mkTwelfWorker(timeoutCallback: () => void): Promise<TwelfWorker> {
-  const worker = new TwelfWorker(timeoutCallback);
+export async function mkTwelfWorker(): Promise<TwelfWorker> {
+  const worker = new TwelfWorker();
   await worker.isReady();
   return worker;
 }
@@ -12,7 +12,7 @@ export class TwelfWorker {
   worker: Worker;
   _readyPromise: Promise<void>;
 
-  constructor(public timeoutCallback: () => void) {
+  constructor() {
     this.worker = new Worker('./assets/worker.js');
     this.worker.onmessage = (msg) => {
       const data: TwelfResponse = msg.data;
@@ -41,16 +41,31 @@ export class TwelfWorker {
     });
     this.worker.postMessage(req);
 
-    const t = setTimeout(() => {
-      this.worker.terminate();
-      (this.timeoutCallback)();
-    }, 2000);
-    const p = await prom;
-    clearTimeout(t);
-    if (p.t != 'execResponse') {
-      throw new Error(`expected execReponse but got ${p.t}`);
-    }
-    return p.response;
+    return new Promise<TwelfExecResponse>((res, rej) => {
+      console.log('setting timer');
+      const t = setTimeout(() => {
+        console.log('timer reached');
+        this.worker.terminate();
+        res({
+          status: { t: 'timeout' },
+          // XXX we're missing output and errors
+          output: [],
+          errors: [],
+        });
+      }, 2000);
+
+      const makeRequest = async () => {
+        const p = await prom;
+        if (p.t != 'execResponse') {
+          throw new Error(`expected execReponse but got ${p.t}`);
+        }
+        console.log('clearing timer');
+        clearTimeout(t);
+        res(p.response);
+      };
+
+      makeRequest();
+    });
   }
 
   isReady(): Promise<void> {