Method requestResendResult

static/panes/diff.ts:447–457

(id: number | string)

    }

    requestResendResult(id: number | string) {
        if (typeof id === 'string') {
            const p = id.indexOf('_exec');
            if (p !== -1) {
                const execId = Number.parseInt(id.substr(0, p), 10);
                this.eventHub.emit('resendExecution', execId);
            }
        } else {
            this.eventHub.emit('resendCompilation', id);
        }
    }

    refreshDiffOptions(id: number | string, compiler: CompilerInfo, result: CompilationResult) {
        const lhsextraoptions: DiffOption[] = [];