[lint addon] Add option to disable automatic linting

... and export (via defineExtension) a method to explicitly trigger
linting from user code.

addon/lint/lint.js

@@ -187,7 +187,9 @@
   CodeMirror.defineOption("lint", false, function(cm, val, old) {
     if (old && old != CodeMirror.Init) {
       clearMarks(cm);
-      cm.off("change", onChange);
+      if (!state.options.disableLintOnChange) {
+        cm.off("change", onChange);
+      }
       CodeMirror.off(cm.getWrapperElement(), "mouseover", cm.state.lint.onMouseOver);
       clearTimeout(cm.state.lint.timeout);
       delete cm.state.lint;
@@ -197,11 +199,19 @@
       var gutters = cm.getOption("gutters"), hasLintGutter = false;
       for (var i = 0; i < gutters.length; ++i) if (gutters[i] == GUTTER_ID) hasLintGutter = true;
       var state = cm.state.lint = new LintState(cm, parseOptions(cm, val), hasLintGutter);
-      cm.on("change", onChange);
+      if (!state.options.disableLintOnChange) {
+        cm.on("change", onChange);
+      }
       if (state.options.tooltips != false)
         CodeMirror.on(cm.getWrapperElement(), "mouseover", state.onMouseOver);
 
       startLinting(cm);
     }
   });
+
+  CodeMirror.defineExtension("performLint", function(cm) {
+    var state = cm.state.lint;
+    if (!state) return;
+    startLinting(cm);
+  });
 });

demo/lint.html

@@ -164,8 +164,12 @@ li.last {
     lineNumbers: true,
     mode: "css",
     gutters: ["CodeMirror-lint-markers"],
-    lint: true
+    lint: {
+      disableLintOnChange: true
+    }
   });
+  // Performing the lint every 5 seconds on the css editor:
+  setInterval(function() {editor_css.performLint(editor_css);}, 5000);
 </script>
 
   </article>

doc/manual.html

@@ -2689,6 +2689,10 @@ editor.setOption("extraKeys", {
       which is a callback to pass the array to. Depends
       on <code>addon/lint/lint.css</code>. A demo can be
       found <a href="../demo/lint.html">here</a>.</dd>
+      <dd>Linting on every change can be disabled using <code>disableLintOnChange</code>
+      option. One can then perform the lint operation using the <code>performLint</code>
+      method which is defined as an extension. This method takes an editor instance
+      as its parameter.</dd>
 
       <dt id="addon_mark-selection"><a href="../addon/selection/mark-selection.js"><code>selection/mark-selection.js</code></a></dt>
       <dd>Causes the selected text to be marked with the CSS class