add setFontSize method to the editor. fix #315

This commit is contained in:
Fabian Jakobs 2011-06-29 08:44:07 +00:00
commit b1b22e2827
2 changed files with 35 additions and 31 deletions

View file

@ -220,15 +220,19 @@ var Editor =function(renderer, session) {
this.getTheme = function() { this.getTheme = function() {
return this.renderer.getTheme(); return this.renderer.getTheme();
} };
this.setStyle = function(style) { this.setStyle = function(style) {
this.renderer.setStyle(style) this.renderer.setStyle(style);
}; };
this.unsetStyle = function(style) { this.unsetStyle = function(style) {
this.renderer.unsetStyle(style) this.renderer.unsetStyle(style);
} };
this.setFontSize = function(size) {
this.container.style.fontSize = size;
};
this.$highlightBrackets = function() { this.$highlightBrackets = function() {
if (this.session.$bracketHighlight) { if (this.session.$bracketHighlight) {

View file

@ -83,9 +83,9 @@ var Split = function(container, theme, splits) {
}.bind(this)); }.bind(this));
this.$editors.push(editor); this.$editors.push(editor);
editor.container.style.fontSize = this.$fontSize; editor.setFontSize(this.$fontSize);
return editor; return editor;
} };
this.setSplits = function(splits) { this.setSplits = function(splits) {
var editor; var editor;
@ -97,9 +97,9 @@ var Split = function(container, theme, splits) {
return; return;
} else if (splits > this.$splits) { } else if (splits > this.$splits) {
while (this.$splits < this.$editors.length && this.$splits < splits) { while (this.$splits < this.$editors.length && this.$splits < splits) {
var editor = this.$editors[this.$splits]; editor = this.$editors[this.$splits];
this.$container.appendChild(editor.container); this.$container.appendChild(editor.container);
editor.container.style.fontSize = this.$fontSize; editor.setFontSize(this.$fontSize);
this.$splits ++; this.$splits ++;
} }
while (this.$splits < splits) { while (this.$splits < splits) {
@ -114,50 +114,50 @@ var Split = function(container, theme, splits) {
} }
} }
this.resize(); this.resize();
} };
this.getSplits = function() { this.getSplits = function() {
return this.$splits; return this.$splits;
} };
this.getEditor = function(idx) { this.getEditor = function(idx) {
return this.$editors[idx]; return this.$editors[idx];
} };
this.getCurrentEditor = function() { this.getCurrentEditor = function() {
return this.$cEditor; return this.$cEditor;
} };
this.focus = function() { this.focus = function() {
this.$cEditor.focus(); this.$cEditor.focus();
} };
this.blur = function() { this.blur = function() {
this.$cEditor.blur(); this.$cEditor.blur();
} };
this.setTheme = function(theme) { this.setTheme = function(theme) {
this.$editors.forEach(function(editor) { this.$editors.forEach(function(editor) {
editor.setTheme(theme); editor.setTheme(theme);
}); });
} };
this.setKeyboardHandler = function(keybinding) { this.setKeyboardHandler = function(keybinding) {
this.$editors.forEach(function(editor) { this.$editors.forEach(function(editor) {
editor.setKeyboardHandler(keybinding); editor.setKeyboardHandler(keybinding);
}); });
} };
this.forEach = function(callback, scope) { this.forEach = function(callback, scope) {
this.$editors.forEach(callback, scope); this.$editors.forEach(callback, scope);
} };
this.setFontSize = function(size) { this.setFontSize = function(size) {
this.$fontSize = size; this.$fontSize = size;
this.forEach(function(editor) { this.forEach(function(editor) {
editor.container.style.fontSize = size; editor.setFontSize(size);
}); });
} };
this.$cloneSession = function(session) { this.$cloneSession = function(session) {
var s = new EditSession(session.getDocument(), session.getMode()); var s = new EditSession(session.getDocument(), session.getMode());
@ -184,7 +184,7 @@ var Split = function(container, theme, splits) {
s.$foldData = session.$cloneFoldData(); s.$foldData = session.$cloneFoldData();
return s; return s;
} };
this.setSession = function(session, idx) { this.setSession = function(session, idx) {
var editor var editor
@ -210,11 +210,11 @@ var Split = function(container, theme, splits) {
// Return the session set on the editor. This might be a cloned one. // Return the session set on the editor. This might be a cloned one.
return session; return session;
} };
this.getOriantation = function() { this.getOriantation = function() {
return this.$oriantation; return this.$oriantation;
} };
this.setOriantation = function(oriantation) { this.setOriantation = function(oriantation) {
if (this.$oriantation == oriantation) { if (this.$oriantation == oriantation) {
@ -222,7 +222,7 @@ var Split = function(container, theme, splits) {
} }
this.$oriantation = oriantation; this.$oriantation = oriantation;
this.resize(); this.resize();
} };
this.resize = function() { this.resize = function() {
var width = this.$container.clientWidth; var width = this.$container.clientWidth;
@ -244,13 +244,13 @@ var Split = function(container, theme, splits) {
for (var i = 0; i < this.$splits; i++) { for (var i = 0; i < this.$splits; i++) {
editor = this.$editors[i]; editor = this.$editors[i];
editor.container.style.width = width + "px"; editor.container.style.width = width + "px";
editor.container.style.top = i * editorHeight + "px" editor.container.style.top = i * editorHeight + "px";
editor.container.style.left = "0px"; editor.container.style.left = "0px";
editor.container.style.height = editorHeight + "px"; editor.container.style.height = editorHeight + "px";
editor.resize(); editor.resize();
} }
} }
} };
}).call(Split.prototype); }).call(Split.prototype);
@ -262,33 +262,33 @@ function UndoManagerProxy(undoManager, session) {
(function() { (function() {
this.execute = function(options) { this.execute = function(options) {
this.$u.execute(options); this.$u.execute(options);
} };
this.undo = function() { this.undo = function() {
var selectionRange = this.$u.undo(true); var selectionRange = this.$u.undo(true);
if (selectionRange) { if (selectionRange) {
this.$doc.selection.setSelectionRange(selectionRange); this.$doc.selection.setSelectionRange(selectionRange);
} }
} };
this.redo = function() { this.redo = function() {
var selectionRange = this.$u.redo(true); var selectionRange = this.$u.redo(true);
if (selectionRange) { if (selectionRange) {
this.$doc.selection.setSelectionRange(selectionRange); this.$doc.selection.setSelectionRange(selectionRange);
} }
} };
this.reset = function() { this.reset = function() {
this.$u.reset(); this.$u.reset();
} };
this.hasUndo = function() { this.hasUndo = function() {
return this.$u.hasUndo(); return this.$u.hasUndo();
} };
this.hasRedo = function() { this.hasRedo = function() {
return this.$u.hasRedo(); return this.$u.hasRedo();
} };
}).call(UndoManagerProxy.prototype); }).call(UndoManagerProxy.prototype);
exports.Split = Split; exports.Split = Split;