Make line widget handles objects with methods. Handle widget height better

Closes #1147

Widget handles now have .clear() and .changed() methods. The second informs CodeMirror
that the widget changed, and causes it to recompute the line height for the widget's
line.

Fixes some sloppiness in the tracking of widget heights.

Author: marijnh

doc/manual.html

@@ -978,12 +978,15 @@ Programming API
       CodeMirror-specific CSS classes, and those classes might in some
       cases affect it. This method returns an object that represents
       the widget placement. It'll have a <code>linecode> property
-      pointing at the line handle that it is associated with, and it
-      can be passed to <code>removeLineWidgetcode> to remove the
-      widget.dd>
-
-      <dt id="removeLineWidget"><code>removeLineWidget(widget)code>dt>
-      <dd>Removes the given line widget.dd>
+      pointing at the line handle that it is associated with, and the following methods:
+        <dl>
+          <dt id="widget_clear"><code>clear()code>dt><dd>Removes the widget.dd>
+          <dt id="widget_changed"><code>changed()code>dt><dd>Call
+          this if you made some change to the widget's DOM node that
+          might affect its height. It'll force CodeMirror to update
+          the height of the line that contains the widget.dd>
+        dl>
+      dd>
 
       <dt id="posFromIndex"><code>posFromIndex(index) → objectcode>dt>
       <dd>Calculates and returns a <code>{line, ch}code> object for a

lib/codemirror.js

@@ -497,8 +497,12 @@ window.CodeMirror = (function() {
       }
       var diff = node.lineObj.height - height;
       if (height < 2) height = textHeight(display);
-      if (diff > .001 || diff < -.001)
+      if (diff > .001 || diff < -.001) {
         updateLineHeight(node.lineObj, height);
+        var widgets = node.lineObj.widgets;
+        if (widgets) for (var i = 0; i < widgets.length; ++i)
+          widgets[i].height = widgets[i].node.offsetHeight;
+      }
     }
     display.viewOffset = heightAtLine(cm, getLine(doc, from));
     // Position the mover div to align with the current virtual scroll position
@@ -978,7 +982,7 @@ window.CodeMirror = (function() {
   // Context is one of "line", "div" (display.lineDiv), "local"/null (editor), or "page"
   function intoCoordSystem(cm, lineObj, rect, context) {
     if (lineObj.widgets) for (var i = 0; i < lineObj.widgets.length; ++i) if (lineObj.widgets[i].above) {
-      var size = lineObj.widgets[i].node.offsetHeight;
+      var size = widgetHeight(lineObj.widgets[i]);
       rect.top += size; rect.bottom += size;
     }
     if (context == "line") return rect;
@@ -2597,25 +2601,10 @@ window.CodeMirror = (function() {
     }),
 
     addLineWidget: operation(null, function(handle, node, options) {
-      var widget = options || {};
-      widget.node = node;
-      if (widget.noHScroll) this.display.alignWidgets = true;
-      changeLine(this, handle, function(line) {
-        (line.widgets || (line.widgets = [])).push(widget);
-        widget.line = line;
-        return true;
-      });
-      return widget;
+      return addLineWidget(this, handle, node, options);
     }),
 
-    removeLineWidget: operation(null, function(widget) {
-      var ws = widget.line.widgets, no = lineNo(widget.line);
-      if (no == null || !ws) return;
-      for (var i = 0; i < ws.length; ++i) if (ws[i] == widget) ws.splice(i--, 1);
-      var newHeight = widget.node.offsetHeight ? widget.line.height - widget.node.offsetHeight : textHeight(this.display);
-      updateLineHeight(widget.line, newHeight);
-      regChange(this, no, no + 1);
-    }),
+    removeLineWidget: function(widget) { widget.remove(); },
 
     lineInfo: function(line) {
       if (typeof line == "number") {
@@ -3587,6 +3576,59 @@ window.CodeMirror = (function() {
     line.markedSpans = spans;
   }
 
+  // LINE WIDGETS
+
+  var LineWidget = CodeMirror.LineWidget = function(cm, node, options) {
+    for (var opt in options) if (options.hasOwnProperty(opt))
+      this[opt] = options[opt];
+    this.cm = cm;
+    this.node = node;
+  };
+  function widgetOperation(f) {
+    return function() {
+      startOperation(this.cm);
+      try {var result = f.apply(this, arguments);}
+      finally {endOperation(this.cm);}
+      return result;
+    };
+  }
+  LineWidget.prototype.clear = widgetOperation(function() {
+    var ws = this.line.widgets, no = lineNo(this.line);
+    if (no == null || !ws) return;
+    for (var i = 0; i < ws.length; ++i) if (ws[i] == this) ws.splice(i--, 1);
+    updateLineHeight(this.line, Math.max(0, this.line.height - widgetHeight(this)));
+    regChange(this.cm, no, no + 1);
+  });
+  LineWidget.prototype.changed = widgetOperation(function() {
+    var oldH = this.height;
+    this.height = null;
+    var diff = widgetHeight(this) - oldH;
+    if (!diff) return;
+    updateLineHeight(this.line, this.line.height + diff);
+    var no = lineNo(this.line);
+    regChange(this.cm, no, no + 1);
+  });
+
+  function widgetHeight(widget) {
+    if (widget.height != null) return widget.height;
+    if (!widget.node.parentNode)
+      removeChildrenAndAdd(widget.cm.display.measure, elt("div", [widget.node], null, "position: relative"));
+    return widget.height = widget.node.offsetHeight;
+  }
+
+  function addLineWidget(cm, handle, node, options) {
+    var widget = new LineWidget(cm, node, options);
+    if (widget.noHScroll) cm.display.alignWidgets = true;
+    changeLine(cm, handle, function(line) {
+      (line.widgets || (line.widgets = [])).push(widget);
+      widget.line = line;
+      if (!lineIsHidden(line) || widget.showIfHidden)
+        updateLineHeight(line, line.height + widgetHeight(widget));
+      return true;
+    });
+    return widget;
+  }
+
   // LINE DATA STRUCTURE
 
   // Line objects. These hold state related to a line, including