Module src/ext/options

Settings Menu extension

Provides a settings panel for configuring editor options through an interactive UI. Creates a tabular interface with grouped configuration options including themes, modes, keybindings, font settings, display preferences, and advanced editor behaviors. Supports dynamic option rendering with various input types (dropdowns, checkboxes, number inputs, button bars) and real-time updates.

Usage:

var OptionPanel = require("ace/ext/settings_menu").OptionPanel;
var panel = new OptionPanel(editor);
panel.render();
Copy