Turn into separate plugin
This commit is contained in:
parent
d54921fcc9
commit
6e1398273c
4 changed files with 324 additions and 234 deletions
|
|
@ -362,7 +362,7 @@ bindCheckbox("read_only", function(checked) {
|
|||
|
||||
bindDropdown("split", function(value) {
|
||||
var sp = env.split;
|
||||
if (value == "none") {
|
||||
if (value == "none") {
|
||||
sp.setSplits(1);
|
||||
} else {
|
||||
var newEditor = (sp.getSplits() == 1);
|
||||
|
|
@ -377,6 +377,12 @@ bindDropdown("split", function(value) {
|
|||
}
|
||||
});
|
||||
|
||||
|
||||
bindCheckbox("elastic_tabstops", function(checked) {
|
||||
env.editor.setUseElasticTabstops(checked);
|
||||
});
|
||||
|
||||
|
||||
function synchroniseScrolling() {
|
||||
var s1 = env.split.$editors[0].session;
|
||||
var s2 = env.split.$editors[1].session;
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue