| 12345678910111213141516171819202122232425262728293031323334 | // Because sometimes you need to mark the selected *text*.//// Adds an option 'styleSelectedText' which, when enabled, gives// selected text the CSS class "CodeMirror-selectedtext".(function() {  "use strict";  CodeMirror.defineOption("styleSelectedText", false, function(cm, val, old) {    var prev = old && old != CodeMirror.Init;    if (val && !prev) {      updateSelectedText(cm);      cm.on("cursorActivity", updateSelectedText);    } else if (!val && prev) {      cm.off("cursorActivity", updateSelectedText);      clearSelectedText(cm);      delete cm._selectionMark;    }  });  function clearSelectedText(cm) {    if (cm._selectionMark) cm._selectionMark.clear();  }  function updateSelectedText(cm) {    clearSelectedText(cm);    if (cm.somethingSelected())      cm._selectionMark = cm.markText(cm.getCursor("start"), cm.getCursor("end"),                                      {className: "CodeMirror-selectedtext"});    else      cm._selectionMark = null;  }})();
 |