Function pushSelectionToHistory

tools/pythonauto/static/codemirrorepl/codemirror.js:6663–6667

(sel, dest)

  }

  function pushSelectionToHistory(sel, dest) {
    var top = lst(dest);
    if (!(top && top.ranges && top.equals(sel)))
      dest.push(sel);
  }

  // Used to store marked span information in the history.
  function attachLocalSpans(doc, change, from, to) {