From b1b22e282745d24f16e2f74c61a38b71d4f82639 Mon Sep 17 00:00:00 2001
From: Fabian Jakobs <fabian.jakobs@web.de>
Date: Wed, 29 Jun 2011 08:44:07 +0000
Subject: [PATCH] add setFontSize method to the editor. fix #315

---
 lib/ace/editor.js | 12 +++++++----
 lib/ace/split.js  | 54 +++++++++++++++++++++++------------------------
 2 files changed, 35 insertions(+), 31 deletions(-)

diff --git a/lib/ace/editor.js b/lib/ace/editor.js
index 3901618e..c1a190c5 100644
--- a/lib/ace/editor.js
+++ b/lib/ace/editor.js
@@ -220,15 +220,19 @@ var Editor =function(renderer, session) {
 
     this.getTheme = function() {
         return this.renderer.getTheme();
-    }
+    };
 
     this.setStyle = function(style) {
-        this.renderer.setStyle(style)
+        this.renderer.setStyle(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() {
         if (this.session.$bracketHighlight) {
diff --git a/lib/ace/split.js b/lib/ace/split.js
index e6c671ca..4134cbd6 100644
--- a/lib/ace/split.js
+++ b/lib/ace/split.js
@@ -83,9 +83,9 @@ var Split = function(container, theme, splits) {
         }.bind(this));
 
         this.$editors.push(editor);
-        editor.container.style.fontSize = this.$fontSize;
+        editor.setFontSize(this.$fontSize);
         return editor;
-    }
+    };
 
     this.setSplits = function(splits) {
         var editor;
@@ -97,9 +97,9 @@ var Split = function(container, theme, splits) {
             return;
         } else if (splits > this.$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);
-                editor.container.style.fontSize = this.$fontSize;
+                editor.setFontSize(this.$fontSize);
                 this.$splits ++;
             }
             while (this.$splits < splits) {
@@ -114,50 +114,50 @@ var Split = function(container, theme, splits) {
             }
         }
         this.resize();
-    }
+    };
 
     this.getSplits = function() {
         return this.$splits;
-    }
+    };
 
     this.getEditor = function(idx) {
         return this.$editors[idx];
-    }
+    };
 
     this.getCurrentEditor = function() {
         return this.$cEditor;
-    }
+    };
 
     this.focus = function() {
         this.$cEditor.focus();
-    }
+    };
 
     this.blur = function() {
         this.$cEditor.blur();
-    }
+    };
 
     this.setTheme = function(theme) {
         this.$editors.forEach(function(editor) {
             editor.setTheme(theme);
         });
-    }
+    };
 
     this.setKeyboardHandler = function(keybinding) {
         this.$editors.forEach(function(editor) {
             editor.setKeyboardHandler(keybinding);
         });
-    }
+    };
 
     this.forEach = function(callback, scope) {
         this.$editors.forEach(callback, scope);
-    }
+    };
 
     this.setFontSize = function(size) {
         this.$fontSize = size;
         this.forEach(function(editor) {
-           editor.container.style.fontSize = size;
+           editor.setFontSize(size);
         });
-    }
+    };
 
     this.$cloneSession = function(session) {
         var s = new EditSession(session.getDocument(), session.getMode());
@@ -184,7 +184,7 @@ var Split = function(container, theme, splits) {
         s.$foldData = session.$cloneFoldData();
 
         return s;
-    }
+    };
 
     this.setSession = function(session, idx) {
         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 session;
-    }
+    };
 
     this.getOriantation = function() {
         return this.$oriantation;
-    }
+    };
 
     this.setOriantation = function(oriantation) {
         if (this.$oriantation == oriantation) {
@@ -222,7 +222,7 @@ var Split = function(container, theme, splits) {
         }
         this.$oriantation = oriantation;
         this.resize();
-    }
+    };
 
     this.resize = function() {
         var width = this.$container.clientWidth;
@@ -244,13 +244,13 @@ var Split = function(container, theme, splits) {
             for (var i = 0; i < this.$splits; i++) {
                 editor = this.$editors[i];
                 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.height = editorHeight + "px";
                 editor.resize();
             }
         }
-    }
+    };
 
 }).call(Split.prototype);
 
@@ -262,33 +262,33 @@ function UndoManagerProxy(undoManager, session) {
 (function() {
     this.execute = function(options) {
         this.$u.execute(options);
-    }
+    };
 
     this.undo = function() {
         var selectionRange = this.$u.undo(true);
         if (selectionRange) {
             this.$doc.selection.setSelectionRange(selectionRange);
         }
-    }
+    };
 
     this.redo = function() {
         var selectionRange = this.$u.redo(true);
         if (selectionRange) {
             this.$doc.selection.setSelectionRange(selectionRange);
         }
-    }
+    };
 
     this.reset = function() {
         this.$u.reset();
-    }
+    };
 
     this.hasUndo = function() {
         return this.$u.hasUndo();
-    }
+    };
 
     this.hasRedo = function() {
         return this.$u.hasRedo();
-    }
+    };
 }).call(UndoManagerProxy.prototype);
 
 exports.Split = Split;