add fixedWidthGutter option

This commit is contained in:
nightwing 2013-08-26 18:46:42 +04:00
commit 244e1462e8
3 changed files with 10 additions and 1 deletions

View file

@ -2385,6 +2385,7 @@ config.defineOptions(Editor.prototype, "editor", {
maxLines: "renderer",
minLines: "renderer",
scrollPastEnd: "renderer",
fixedWidthGutter: "renderer",
scrollSpeed: "$mouseHandler",
dragDelay: "$mouseHandler",

View file

@ -168,7 +168,7 @@ var Gutter = function(parentEl) {
this.element = dom.setInnerHtml(this.element, html.join(""));
this.element.style.height = config.minHeight + "px";
if (this.session.$useWrapMode)
if (this.$fixedWidth || this.session.$useWrapMode)
lastLineNumber = this.session.getLength();
var gutterWidth = ("" + lastLineNumber).length * config.characterWidth;
@ -181,6 +181,8 @@ var Gutter = function(parentEl) {
}
};
this.$fixedWidth = false;
this.$showFoldWidgets = true;
this.setShowFoldWidgets = function(show) {
if (show)

View file

@ -1655,6 +1655,12 @@ config.defineOptions(VirtualRenderer.prototype, "renderer", {
},
initialValue: 0,
handlesSet: true
},
fixedWidthGutter: {
set: function(val) {
this.gutterLayer.fixedWidth = !!val;
this.$loop.schedule(this.CHANGE_GUTTER);
}
}
});