@@ -219,7 +219,7 @@ coverage.pyfile_ready = function () {
219
219
220
220
// If we're directed to a particular line number, highlight the line.
221
221
var frag = location . hash ;
222
- if ( frag . length > 2 && frag [ 1 ] === 't' ) {
222
+ if ( frag . length > 2 && frag [ 1 ] === "t" ) {
223
223
document . querySelector ( frag ) . closest ( ".n" ) . classList . add ( "highlight" ) ;
224
224
coverage . set_sel ( parseInt ( frag . substr ( 2 ) , 10 ) ) ;
225
225
} else {
@@ -533,14 +533,14 @@ coverage.scroll_window = function (to_pos) {
533
533
534
534
coverage . init_scroll_markers = function ( ) {
535
535
// Init some variables
536
- coverage . lines_len = document . querySelectorAll ( ' #source > p' ) . length ;
536
+ coverage . lines_len = document . querySelectorAll ( " #source > p" ) . length ;
537
537
538
538
// Build html
539
539
coverage . build_scroll_markers ( ) ;
540
540
} ;
541
541
542
542
coverage . build_scroll_markers = function ( ) {
543
- const temp_scroll_marker = document . getElementById ( ' scroll_marker' )
543
+ const temp_scroll_marker = document . getElementById ( " scroll_marker" )
544
544
if ( temp_scroll_marker ) temp_scroll_marker . remove ( ) ;
545
545
// Don't build markers if the window has no scroll bar.
546
546
if ( document . body . scrollHeight <= window . innerHeight ) {
@@ -554,8 +554,8 @@ coverage.build_scroll_markers = function () {
554
554
555
555
const scroll_marker = document . createElement ( "div" ) ;
556
556
scroll_marker . id = "scroll_marker" ;
557
- document . getElementById ( ' source' ) . querySelectorAll (
558
- ' p.show_run, p.show_mis, p.show_exc, p.show_exc, p.show_par'
557
+ document . getElementById ( " source" ) . querySelectorAll (
558
+ " p.show_run, p.show_mis, p.show_exc, p.show_exc, p.show_par"
559
559
) . forEach ( element => {
560
560
const line_top = Math . floor ( element . offsetTop * marker_scale ) ;
561
561
const line_number = parseInt ( element . querySelector ( ".n a" ) . id . substr ( 1 ) ) ;
@@ -582,21 +582,21 @@ coverage.build_scroll_markers = function () {
582
582
} ;
583
583
584
584
coverage . wire_up_sticky_header = function ( ) {
585
- const header = document . querySelector ( ' header' ) ;
585
+ const header = document . querySelector ( " header" ) ;
586
586
const header_bottom = (
587
- header . querySelector ( ' .content h2' ) . getBoundingClientRect ( ) . top -
587
+ header . querySelector ( " .content h2" ) . getBoundingClientRect ( ) . top -
588
588
header . getBoundingClientRect ( ) . top
589
589
) ;
590
590
591
591
function updateHeader ( ) {
592
592
if ( window . scrollY > header_bottom ) {
593
- header . classList . add ( ' sticky' ) ;
593
+ header . classList . add ( " sticky" ) ;
594
594
} else {
595
- header . classList . remove ( ' sticky' ) ;
595
+ header . classList . remove ( " sticky" ) ;
596
596
}
597
597
}
598
598
599
- window . addEventListener ( ' scroll' , updateHeader ) ;
599
+ window . addEventListener ( " scroll" , updateHeader ) ;
600
600
updateHeader ( ) ;
601
601
} ;
602
602
0 commit comments