diff options
author | Ned Batchelder <ned@nedbatchelder.com> | 2016-01-31 08:17:41 -0500 |
---|---|---|
committer | Ned Batchelder <ned@nedbatchelder.com> | 2016-01-31 08:17:41 -0500 |
commit | b920b36476caa848e1773063e8bdc15781ff32c9 (patch) | |
tree | 9b24298c27d0b5ede5d96785517451dc52744928 /coverage/htmlfiles/coverage_html.js | |
parent | 61a45f1d49bc2bc75013205618daebc2a23e1769 (diff) | |
download | python-coveragepy-b920b36476caa848e1773063e8bdc15781ff32c9.tar.gz |
Simplify and improve the accuracy of the scroll markers
Diffstat (limited to 'coverage/htmlfiles/coverage_html.js')
-rw-r--r-- | coverage/htmlfiles/coverage_html.js | 32 |
1 files changed, 18 insertions, 14 deletions
diff --git a/coverage/htmlfiles/coverage_html.js b/coverage/htmlfiles/coverage_html.js index 2fbd150..8bbf193 100644 --- a/coverage/htmlfiles/coverage_html.js +++ b/coverage/htmlfiles/coverage_html.js @@ -532,7 +532,6 @@ coverage.resize_scroll_markers = function () { var c = coverage, min_line_height = 3, max_line_height = 10, - previous_line = 0, visible_window_h = $(window).height(); $('#scroll_marker').remove(); @@ -543,9 +542,8 @@ coverage.resize_scroll_markers = function () { $("body").append("<div id='scroll_marker'> </div>"); var scroll_marker = $('#scroll_marker'), - header_amend = Math.round(c.header_h*scroll_marker.height()/c.body_h), - line_height = scroll_marker.height()/c.lines_len, - general_height = 0; + marker_scale = scroll_marker.height() / c.body_h, + line_height = scroll_marker.height() / c.lines_len; // Line height must be between the extremes. if (line_height > min_line_height) { @@ -557,26 +555,32 @@ coverage.resize_scroll_markers = function () { line_height = min_line_height; } + var previous_line = -99, + last_mark, + last_top; + c.missed_lines.each(function () { - var line_position = Math.round($(this).offset().top*scroll_marker.height()/c.body_h); - var id_name = $(this).attr('id'), - line_number = id_name.substring(1, id_name.length); - if (line_number === parseInt(previous_line)+1) { - // If this solid missed block just make previous line higher. - $('#m' + previous_line).attr('id', 'm' + line_number).css({ - 'height': "+=" + line_height + var line_top = Math.round($(this).offset().top * marker_scale), + id_name = $(this).attr('id'), + line_number = parseInt(id_name.substring(1, id_name.length)); + + if (line_number === previous_line + 1) { + // If this solid missed block just make previous mark higher. + last_mark.css({ + 'height': line_top + line_height - last_top }); } else { // Add colored line in scroll_marker block. scroll_marker.append('<div id="m' + line_number + '" class="marker"></div>'); - $('#m' + line_number).css({ + last_mark = $('#m' + line_number); + last_mark.css({ 'height': line_height, - 'top': line_position - header_amend - general_height + 'top': line_top }); + last_top = line_top; } - general_height += line_height; previous_line = line_number; }); }; |