Merge pull request #2052 from ajaxorg/double_tap

fix Double tapping to select words doesn't work reliably
This commit is contained in:
Lennart Kats 2014-07-21 14:06:19 +02:00
commit b71a09d8d0
4 changed files with 19 additions and 45 deletions

View file

@ -415,28 +415,11 @@ bindDropdown("folding", function(value) {
});
bindDropdown("soft_wrap", function(value) {
var session = env.editor.session;
var renderer = env.editor.renderer;
switch (value) {
case "off":
session.setUseWrapMode(false);
renderer.setPrintMarginColumn(80);
break;
case "free":
session.setUseWrapMode(true);
session.setWrapLimitRange(null, null);
renderer.setPrintMarginColumn(80);
break;
default:
session.setUseWrapMode(true);
var col = parseInt(value, 10);
session.setWrapLimitRange(col, col);
renderer.setPrintMarginColumn(col);
}
env.editor.setOption("wrap", value);
});
bindCheckbox("select_style", function(checked) {
env.editor.setSelectionStyle(checked ? "line" : "text");
env.editor.setOption("selectionStyle", checked ? "line" : "text");
});
bindCheckbox("highlight_active", function(checked) {