Function scrollToAnchor

data/codebrowser.js:1201–1221

(anchor, isLink)

    // fix scrolling to an anchor because of the header
    // isLink tells us if we are here because a link was cliked
    function scrollToAnchor(anchor, isLink) {
        var target = $("#" + escape_selector(anchor));
        if (target.length) {
            //Smooth scrolling and let back go to the last location
            var contentTop = $("#content").offset().top;
            if (parseInt(anchor)) {
                // if the anchor is a line number, (or a function local) we want to give a bit more
                // context on top
                contentTop += target.height() * 7; // 7 lines
            }

            if (isLink) {
            //   history.replaceState({contentTop: contentTop, bodyTop: $("body").scrollTop() }, undefined)
                history.pushState({bodyTop: target.offset().top - contentTop},
                                    document.title + "**" + anchor,
                                    window.location.pathname + "#" + anchor);
            }
            //     $("#content").animate({scrollTop:target.position().top + contentTop }, 300);
            $("html,body").animate({scrollTop:target.offset().top - contentTop  }, isLink ? 300 : 1);
        }
    }

    window.onpopstate = function (e) {
        if (!e.state)