Method updateConfigSelection

Extension/ui/settings.ts:349–369

(message: any)

    }

    private updateConfigSelection(message: any): void {
        this.updating = true;
        try {
            const list: HTMLSelectElement = <HTMLSelectElement>document.getElementById(elementId.configSelection);

            // Clear list before updating
            list.options.length = 0;

            // Update list
            for (const name of message.selections) {
                const option: HTMLOptionElement = document.createElement("option");
                option.text = name;
                option.value = name;
                list.append(option);
            }

            list.selectedIndex = message.selectedIndex;
        } finally {
            this.updating = false;
        }
    }

    private setKnownCompilers(compilers: string[]): void {
        this.updating = true;