Function setSelectionUser

tools/pythonauto/static/codemirrorepl/codemirrorepl.js:1367–1375

(from, to)

            else shiftSelecting = null;
        }
        function setSelectionUser(from, to) {
            var sh = shiftSelecting && clipPos(shiftSelecting);
            if (sh) {
                if (posLess(sh, from)) from = sh;
                else if (posLess(to, sh)) to = sh;
            }
            setSelection(from, to);
            userSelChange = true;
        }
        // Update the selection. Last two args are only used by
        // updateLines, since they have to be expressed in the line
        // numbers before the update.