Skip to content

Commit

Permalink
Make timeout actually work
Browse files Browse the repository at this point in the history
  • Loading branch information
jcreedcmu committed Mar 15, 2024
1 parent a72085e commit 3268617
Show file tree
Hide file tree
Showing 2 changed files with 35 additions and 20 deletions.
14 changes: 7 additions & 7 deletions src/index.ts
Original file line number Diff line number Diff line change
Expand Up @@ -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('');
Expand Down
41 changes: 28 additions & 13 deletions src/twelf-worker.ts
Original file line number Diff line number Diff line change
@@ -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;
}
Expand All @@ -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;
Expand Down Expand Up @@ -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> {
Expand Down

0 comments on commit 3268617

Please sign in to comment.