| 1234567891011121314151617181920212223242526272829303132 | 
							- CodeMirror.newFoldFunction = function(rangeFinder, widget) {
 
-   if (widget == null) widget = "\u2194";
 
-   if (typeof widget == "string") {
 
-     var text = document.createTextNode(widget);
 
-     widget = document.createElement("span");
 
-     widget.appendChild(text);
 
-     widget.className = "CodeMirror-foldmarker";
 
-   }
 
-   return function(cm, pos) {
 
-     if (typeof pos == "number") pos = CodeMirror.Pos(pos, 0);
 
-     var range = rangeFinder(cm, pos);
 
-     if (!range) return;
 
-     var present = cm.findMarksAt(range.from), cleared = 0;
 
-     for (var i = 0; i < present.length; ++i) {
 
-       if (present[i].__isFold) {
 
-         ++cleared;
 
-         present[i].clear();
 
-       }
 
-     }
 
-     if (cleared) return;
 
-     var myWidget = widget.cloneNode(true);
 
-     CodeMirror.on(myWidget, "mousedown", function() {myRange.clear();});
 
-     var myRange = cm.markText(range.from, range.to, {
 
-       replacedWith: myWidget,
 
-       clearOnEnter: true,
 
-       __isFold: true
 
-     });
 
-   };
 
- };
 
 
  |