+ notifyEnvironment: function() {
+ if (this.onChange) this.onChange();
+ // Used by the line-wrapping line-numbering code.
+ if (window.frameElement && window.frameElement.CodeMirror.updateNumbers)
+ window.frameElement.CodeMirror.updateNumbers();
+ },
+