Function setSelection

tools/pythonauto/static/codemirrorepl/codemirror.js:1121–1125

(doc, sel, options)

  // Set a new selection.
  function setSelection(doc, sel, options) {
    if (options && options.origin && doc.cm) doc.cm.curOp.origin = options.origin;
    setSelectionNoUndo(doc, sel, options);
    addSelectionToHistory(doc, doc.sel, doc.cm ? doc.cm.curOp.id : NaN, options);
  }

  function setSelectionNoUndo(doc, sel, options) {
    if (hasHandler(doc, "beforeSelectionChange") || doc.cm && hasHandler(doc.cm, "beforeSelectionChange"))