[active-line addon] Highlight active line even when text is selected

Adds an option to keep the active line highlighted even when text
inside the line is selected.

addon/selection/active-line.js

@@ -3,9 +3,13 @@
 
 // Because sometimes you need to style the cursor's line.
 //
-// Adds an option 'styleActiveLine' which, when enabled, gives the
-// active line's wrapping <div> the CSS class "CodeMirror-activeline",
-// and gives its background <div> the class "CodeMirror-activeline-background".
+// 'styleActiveLine': when enabled, gives the active line's wrapping
+// <div> the CSS class "CodeMirror-activeline", and gives its background
+// <div> the class "CodeMirror-activeline-background".
+//
+// 'styleActiveSelected': An optional parameter of 'styleActiveLine'.
+// When enabled, keeps the active line's styling active even when text is
+// selected within the line. Has no effect if 'styleActiveLine' is not enabled.
 
 (function(mod) {
   if (typeof exports == "object" && typeof module == "object") // CommonJS
@@ -52,7 +56,11 @@
     var active = [];
     for (var i = 0; i < ranges.length; i++) {
       var range = ranges[i];
-      if (!range.empty()) continue;
+      if (cm.getOption('styleActiveLine').styleActiveSelected == true) {
+        if (range.anchor.line != range.head.line) continue;
+      } else {
+        if (!range.empty()) continue;
+      }
       var line = cm.getLineHandleVisualStart(range.head.line);
       if (active[active.length - 1] != line) active.push(line);
     }

demo/activeline.html

@@ -65,14 +65,26 @@
 </rss></textarea></form>
 
     <script>
+var styleActiveSelected = false;
 var editor = CodeMirror.fromTextArea(document.getElementById("code"), {
   mode: "application/xml",
-  styleActiveLine: true,
+  styleActiveLine: {
+    styleActiveSelected: styleActiveSelected
+  },
   lineNumbers: true,
   lineWrapping: true
 });
+
+function toggleSelProp() {
+  styleActiveSelected = !styleActiveSelected;
+  editor.setOption('styleActiveLine', {styleActiveSelected: styleActiveSelected});
+  var label = styleActiveSelected ? 'Disable styleActiveSelected option' : 'Enable styleActiveSelected option';
+  document.getElementById('toggleButton').innerText = label;
+}
 </script>
 
     <p>Styling the current cursor line.</p>
 
+    <button onclick="toggleSelProp()" id="toggleButton">Enable styleActiveSelected option</button>
+
   </article>

doc/manual.html

@@ -2760,12 +2760,26 @@ editor.setOption("extraKeys", {
       like in <a href="../demo/markselection.html">this demo</a>.</dd>
 
       <dt id="addon_active-line"><a href="../addon/selection/active-line.js"><code>selection/active-line.js</code></a></dt>
-      <dd>Defines a <code>styleActiveLine</code> option that, when enabled,
-      gives the wrapper of the active line the class <code>CodeMirror-activeline</code>,
-      adds a background with the class <code>CodeMirror-activeline-background</code>,
-      and adds the class <code>CodeMirror-activeline-gutter</code> to the
-      line's gutter space is enabled. See the
-      <a href="../demo/activeline.html">demo</a>.</dd>
+      <dd>Controls highlighting of the active line.
+        <dd>Defines an option
+        <code>styleActiveLine</code> which, when enabled, gives the wrapper of
+        the active line the class <code>CodeMirror-activeline</code>, adds a
+        background with the class <code>CodeMirror-activeline-background</code>,
+        and adds the class <code>CodeMirror-activeline-gutter</code> to the
+        line's gutter space.
+        </dd>
+        <dd>
+        In addition, defines an option <code>styleActiveSelected</code>,
+        that controls highlighting behavior when selected.
+        <code>styleActiveSelected</code> is an optional parameter of
+        <code>styleActiveLine</code>. If <code>true</code>,
+        the active line will remain highlighted when text within the line is
+        selected. If <code>false</code> or unspecified, the active line will
+        become unhighlighted as soon as text is selected. Has no effect if
+        <code>styleActiveLine</code> is not enabled.
+        </dd>
+        <dd>See the <a href="../demo/activeline.html">demo</a>.</dd>
+      </dd>
 
       <dt id="addon_selection-pointer"><a href="../addon/selection/selection-pointer.js"><code>selection/selection-pointer.js</code></a></dt>
       <dd>Defines a <code>selectionPointer</code> option which you can