Method getDiffableOptions

static/panes/diff.ts:352–394

(picker?: HTMLSelectElement | TomSelect, extraoptions?: DiffOption[])

    }

    getDiffableOptions(picker?: HTMLSelectElement | TomSelect, extraoptions?: DiffOption[]): any[] {
        const options: DiffOption[] = [
            {id: DiffType.ASM.toString(), name: 'Assembly'},
            {id: DiffType.CompilerStdOut.toString(), name: 'Compiler stdout'},
            {id: DiffType.CompilerStdErr.toString(), name: 'Compiler stderr'},
            {id: DiffType.ExecStdOut.toString(), name: 'Execution stdout'},
            {id: DiffType.ExecStdErr.toString(), name: 'Execution stderr'},
            {id: DiffType.GNAT_ExpandedCode.toString(), name: 'GNAT Expanded Code'},
            {id: DiffType.GNAT_Tree.toString(), name: 'GNAT Tree Code'},
        ];

        if (picker?.classList) {
            if (picker.classList.contains('lhsdifftype')) {
                if (this.lhs.difftype === DiffType.DeviceView && this.lhs.extraoption) {
                    options.push({
                        id: encodeSelectizeValue({
                            difftype: DiffType.DeviceView,
                            extraoption: this.lhs.extraoption,
                        }),
                        name: this.lhs.extraoption,
                    });
                }
            } else {
                if (this.rhs.difftype === DiffType.DeviceView && this.rhs.extraoption) {
                    options.push({
                        id: encodeSelectizeValue({
                            difftype: DiffType.DeviceView,
                            extraoption: this.rhs.extraoption,
                        }),
                        name: this.rhs.extraoption,
                    });
                }
            }
        }

        if (extraoptions) {
            for (const option of extraoptions) {
                if (!options.find(existing => existing.id === option.id)) options.push(option);
            }
        }

        return options;
    }

    override getInitialHTML() {
        return $('#diff').html();