notice when the editor changed height, and update accordingly

fixes a bug where an editor with very little text wouldn't update
its gutter on resize

Author: marijnh

lib/codemirror.js

@@ -61,7 +61,7 @@ var CodeMirror = (function() {
     // happened during the operation.
     var updateInput, changes, textChanged, selectionChanged;
     // Current visible range (may be bigger than the view window).
-    var showingFrom = 0, showingTo = 0;
+    var showingFrom = 0, showingTo = 0, lastHeight = 0;
     // editing will hold an object describing the things we put in the
     // textarea, to help figure out whether something changed.
     // bracketHighlighted is used to remember that a backet has been
@@ -654,10 +654,11 @@ var CodeMirror = (function() {
 
       // Position the mover div to align with the lines it's supposed
       // to be showing (which will cover the visible display)
-      var different = from != showingFrom || to != showingTo;
+      var different = from != showingFrom || to != showingTo || lastHeight != wrapper.clientHeight;
       showingFrom = from; showingTo = to;
       mover.style.top = (from * lineHeight()) + "px";
       if (different) {
+        lastHeight = wrapper.clientHeight;
         code.style.height = (lines.length * lineHeight() + 2 * paddingTop()) + "px";
         updateGutter();
       }