Allow applications to listen for the dragleave event.

Author: julienr

doc/manual.html

@@ -657,7 +657,8 @@ <h2>Events</h2>
       <strong>"keydown"</strong>, <strong>"keypress"</strong>,
       <strong>"keyup"</strong>, <strong>"cut"</strong>, <strong>"copy"</strong>, <strong>"paste"</strong>,
       <strong>"dragstart"</strong>, <strong>"dragenter"</strong>,
-      <strong>"dragover"</strong>, <strong>"drop"</strong>
+      <strong>"dragover"</strong>, <strong>"dragleave"</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, or give it a

lib/codemirror.js

@@ -3495,7 +3495,7 @@
       over: function(e) {if (!signalDOMEvent(cm, e)) { onDragOver(cm, e); e_stop(e); }},
       start: function(e){onDragStart(cm, e);},
       drop: operation(cm, onDrop),
-      leave: function() {clearDragCursor(cm);}
+      leave: function(e) {if (!signalDOMEvent(cm, e)) { clearDragCursor(cm); }}
     };
 
     var inp = d.input.getField();