fix toggle gutter

This commit is contained in:
Fabian Jakobs 2011-01-27 19:41:27 +01:00
commit b200db90e8

View file

@ -184,11 +184,11 @@ var VirtualRenderer = function(container, theme) {
/**
* Triggers resize of the editor
*/
this.onResize = function() {
this.onResize = function(force) {
var changes = this.CHANGE_SIZE;
var height = dom.getInnerHeight(this.container);
if (this.$size.height != height) {
if (force || this.$size.height != height) {
this.$size.height = height;
this.scroller.style.height = height + "px";
@ -201,7 +201,7 @@ var VirtualRenderer = function(container, theme) {
}
var width = dom.getInnerWidth(this.container);
if (this.$size.width != width) {
if (force || this.$size.width != width) {
this.$size.width = width;
var gutterWidth = this.showGutter ? this.$gutter.offsetWidth : 0;
@ -262,7 +262,7 @@ var VirtualRenderer = function(container, theme) {
this.setShowGutter = function(show){
this.$gutter.style.display = show ? "block" : "none";
this.showGutter = show;
this.onResize();
this.onResize(true);
}
this.$updatePrintMargin = function() {