Allow DOM events to be ignored by setting codemirrorIgnore

Issue #1681

Author: marijnh

doc/manual.html

@@ -496,7 +496,8 @@ <h2 id="events">Events</h2>
       <strong>"dragover"</strong>, <strong>"drop"</strong>
       (instance: CodeMirror, event: Event)</code></dt>
       <dd>Fired when CodeMirror is handling a DOM event of this type.
-      You can <code>preventDefault</code> the event to signal that
+      You can <code>preventDefault</code> the event, or give it a
+      truthy <code>codemirrorIgnore</code> property, to signal that
       CodeMirror should do no further handling.</dd>
     </dl>
 

lib/codemirror.js

@@ -5251,7 +5251,7 @@ window.CodeMirror = (function() {
 
   function signalDOMEvent(cm, e, override) {
     signal(cm, override || e.type, cm, e);
-    return e_defaultPrevented(e);
+    return e_defaultPrevented(e) || e.codemirrorIgnore;
   }
 
   function fireDelayed() {