Function done

external/.scrollLibs.js:10317–10325

(e)

    }

    function done(e) {
      cm.state.selectingText = false
      counter = Infinity
      e_preventDefault(e)
      display.input.focus()
      off(display.wrapper.ownerDocument, "mousemove", move)
      off(display.wrapper.ownerDocument, "mouseup", up)
      doc.history.lastSelOrigin = null
    }

    var move = operation(cm, function (e) {
      if (e.buttons === 0 || !e_button(e)) {