Function done

tools/pythonauto/static/codemirrorepl/codemirror.js:2697–2704

(e)

    }

    function done(e) {
      counter = Infinity;
      e_preventDefault(e);
      focusInput(cm);
      off(document, "mousemove", move);
      off(document, "mouseup", up);
      doc.history.lastSelOrigin = null;
    }

    var move = operation(cm, function(e) {
      if ((ie && !ie_upto9) ?  !e.buttons : !e_button(e)) done(e);