Editor: add resize grip

edit.html

@@ -132,6 +132,21 @@
 			.CodeMirror-lint-mark-warning {
 				background: none;
 			}
+			.CodeMirror-vscrollbar {
+				margin-bottom: 8px; /* make space for resize-grip */
+			}
+			.resize-grip {
+				position: absolute;
+				display: block;
+				width: 8px;
+				height: 8px;
+				content: " ";
+				right: 0;
+				bottom: 0;
+				z-index: 99;
+				cursor: n-resize;
+				background: linear-gradient(-45deg, transparent 2px, rgba(0,0,0,0.5) 2px, transparent 3px, transparent 4.5px, rgba(0,0,0,0.5) 5px, transparent 5.5px);
+			}
 			/* applies-to */
 			.applies-to {
 				display: flex;

edit.js

@@ -187,6 +187,24 @@ function setupCodeMirror(textarea, index) {
 		}, 0);
 	});
 
+	var resizeGrip = cm.display.wrapper.appendChild(document.createElement("div"));
+	resizeGrip.className = "resize-grip";
+	resizeGrip.addEventListener("mousedown", function(e) {
+		e.preventDefault();
+		var cm = e.target.parentNode.CodeMirror;
+		var minHeight = cm.defaultTextHeight()
+			+ cm.display.lineDiv.offsetParent.offsetTop /* .CodeMirror-lines padding */
+			+ cm.display.wrapper.offsetHeight - cm.display.wrapper.scrollHeight /* borders */;
+		function resize(e) {
+			cm.setSize(null, Math.max(minHeight, cm.display.wrapper.scrollHeight + e.movementY));
+		}
+		document.addEventListener("mousemove", resize);
+		document.addEventListener("mouseup", function resizeStop() {
+			document.removeEventListener("mouseup", resizeStop);
+			document.removeEventListener("mousemove", resize);
+		});
+	});
+
 	editors.splice(index || editors.length, 0, cm);
 	return cm;
 }