diff options
Diffstat (limited to 'coverage/htmlfiles/coverage_html.js')
-rw-r--r-- | coverage/htmlfiles/coverage_html.js | 20 |
1 files changed, 19 insertions, 1 deletions
diff --git a/coverage/htmlfiles/coverage_html.js b/coverage/htmlfiles/coverage_html.js index 30d3a067..514103c7 100644 --- a/coverage/htmlfiles/coverage_html.js +++ b/coverage/htmlfiles/coverage_html.js @@ -276,9 +276,27 @@ coverage.pyfile_ready = function ($) { coverage.assign_shortkeys(); coverage.wire_up_help_panel(); - coverage.init_scroll_markers(); + const sticky = document.querySelector('#sticky_header'); + const header = document.querySelector('header'); + const header_bottom = document.querySelector('header .content .stats').getBoundingClientRect().top; + + function updateHeader() { + if (window.scrollY > header_bottom) { + sticky.classList.add('visible'); + header.classList.add('hidden'); + } else { + sticky.classList.remove('visible'); + header.classList.remove('hidden'); + } + } + + updateHeader(); + window.addEventListener('scroll', function() { + updateHeader(); + }); + // Rebuild scroll markers when the window height changes. $(window).resize(coverage.build_scroll_markers); }; |