diff --git a/demo/startup.js b/demo/startup.js index 3beec19c..60db99a7 100644 --- a/demo/startup.js +++ b/demo/startup.js @@ -166,6 +166,10 @@ exports.launch = function(env) { env.editor.setKeyboardHandler(keybindings[value]); }); + bindDropdown("fontsize", function(value) { + document.getElementById("editor").style["font-size"] = value; + }); + bindCheckbox("select_style", function(checked) { env.editor.setSelectionStyle(checked ? "line" : "text"); }); diff --git a/editor.html b/editor.html index 21d8b70f..c45c9de2 100644 --- a/editor.html +++ b/editor.html @@ -11,7 +11,7 @@ - - + + +
+ - - - + + + @@ -62,6 +62,19 @@
+ + +