add setting to toggle fold mode

This commit is contained in:
Fabian Jakobs 2011-12-05 12:29:17 +01:00
commit 70cef75704
8 changed files with 80 additions and 38 deletions

View file

@ -283,6 +283,7 @@ var docEl = document.getElementById("doc");
var modeEl = document.getElementById("mode");
var wrapModeEl = document.getElementById("soft_wrap");
var themeEl = document.getElementById("theme");
var foldingEl = document.getElementById("folding");
var selectStyleEl = document.getElementById("select_style");
var highlightActiveEl = document.getElementById("highlight_active");
var showHiddenEl = document.getElementById("show_hidden");
@ -324,6 +325,8 @@ function updateUIEditorOptions() {
docEl.value = session.name;
modeEl.value = session.getMode().name || "text";
session.setFoldStyle(foldingEl.value);
if (!session.getUseWrapMode()) {
wrapModeEl.value = "off";
} else {
@ -365,6 +368,10 @@ bindDropdown("fontsize", function(value) {
env.split.setFontSize(value);
});
bindDropdown("folding", function(value) {
env.editor.getSession().setFoldStyle(value);
});
bindDropdown("soft_wrap", function(value) {
var session = env.editor.getSession();
var renderer = env.editor.renderer;
@ -496,7 +503,7 @@ event.addListener(container, "drop", function(e) {
if (window.FileReader) {
var reader = new FileReader();
reader.onload = function(e) {
reader.onload = function() {
env.editor.getSelection().selectAll();
var mode = modesByName.text;