From fa7bfdeb100322bb2a9786b41a27cc9b3b71f484 Mon Sep 17 00:00:00 2001 From: Julian Viereck Date: Fri, 28 Jan 2011 19:17:04 +0800 Subject: [PATCH] Add editor.html Font-Size selection --- demo/startup.js | 4 ++++ editor.html | 39 ++++++++++++++++++++++++++------------- 2 files changed, 30 insertions(+), 13 deletions(-) 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 @@
+ + +