diff --git a/src/index.ts b/src/index.ts index a64db4d..507874c 100644 --- a/src/index.ts +++ b/src/index.ts @@ -4,7 +4,7 @@ import { EditorView, basicSetup } from "codemirror"; import { decode, encode } from "./encoding"; import { twelfHighlightStyle, twelf as twelfMode } from './twelf-mode'; import { Status, TwelfError } from './twelf-worker-types'; -import { mkTwelfWorker } from './twelf-worker'; +import { TwelfWorker, mkTwelfWorker } from './twelf-worker'; function showStatus(status: Status) { const serverStatus = (document.getElementById('server-status') as HTMLDivElement); @@ -82,11 +82,21 @@ 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 = ''; - const worker = await mkTwelfWorker(); + workerRef.worker = await mkTwelfWorker(timeoutCallback); async function execAndShowStatus(text: string): Promise<void> { - const result = await worker.exec(text); + if (workerRef.worker == undefined) { + throw new Error(`twelf worker not ready yet`); + } + const result = await (workerRef.worker).exec(text); 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 e885db1..ab0a35a 100644 --- a/src/twelf-worker.ts +++ b/src/twelf-worker.ts @@ -1,18 +1,18 @@ import { TwelfExecRequest, TwelfExecResponse, TwelfResponse, WithId } from "./twelf-worker-types"; -export async function mkTwelfWorker(): Promise<TwelfWorker> { - const worker = new TwelfWorker(); +export async function mkTwelfWorker(timeoutCallback: () => void): Promise<TwelfWorker> { + const worker = new TwelfWorker(timeoutCallback); await worker.isReady(); return worker; } -class TwelfWorker { +export class TwelfWorker { requestIdCounter: number = 0; responseMap: Record<number, (result: TwelfResponse) => void>; worker: Worker; _readyPromise: Promise<void>; - constructor() { + constructor(public timeoutCallback: () => void) { this.worker = new Worker('./assets/worker.js'); this.worker.onmessage = (msg) => { const data: TwelfResponse = msg.data; @@ -40,7 +40,13 @@ class TwelfWorker { this.responseMap[req.id] = res; }); 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}`); }