diff options
Diffstat (limited to 'coverage/htmlfiles/coverage_html.js')
| -rw-r--r-- | coverage/htmlfiles/coverage_html.js | 73 |
1 files changed, 73 insertions, 0 deletions
diff --git a/coverage/htmlfiles/coverage_html.js b/coverage/htmlfiles/coverage_html.js index bd6a875..fe12636 100644 --- a/coverage/htmlfiles/coverage_html.js +++ b/coverage/htmlfiles/coverage_html.js @@ -264,6 +264,8 @@ coverage.pyfile_ready = function ($) { coverage.assign_shortkeys(); coverage.wire_up_help_panel(); + + coverage.init_scroll_markers(); }; coverage.toggle_lines = function (btn, cls) { @@ -510,3 +512,74 @@ coverage.scroll_window = function (to_pos) { coverage.finish_scrolling = function () { $("html,body").stop(true, true); }; + +coverage.init_scroll_markers = function(){ + var c = coverage; + // Init some variables + c.lines_len = $('td.text p').length; + c.body_h = $('body').height(); + c.header_h = $('div#header').height(); + c.missed_lines = $('td.text p.mis'); + + // Build html + c.resize_scroll_markers(); + +} + +coverage.resize_scroll_markers = function(){ + var c = coverage, + min_height = 3 + max_height = 10, + previous_line = 0, + visible_window_h = $(window).height(); + $('#scroll_marker').remove(); + // Don't build markers if window hasn't scroll + if (c.body_h<=visible_window_h){ + return false; + } + + $("body").append("<div id='scroll_marker'> </div>"); + var scroll_marker = $('#scroll_marker'); + scroll_marker.css({ + 'height':visible_window_h+'px' + }); + var header_amend = Math.round(c.header_h*scroll_marker.height()/c.body_h), + line_height = scroll_marker.height()/c.lines_len, + general_height = 0; + + // Line height must be between the extremums + if (line_height>min_height){ + if (line_height>max_height){ + line_height= max_height + } + }else{ + line_height = min_height + } + + 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 + }); + }else { + // Add colored line in scroll_marker block + scroll_marker.append('<div id="m' + line_number + '" class="marker"></div>'); + $('#m' + line_number).css({ + 'height': line_height , + 'top': line_position- header_amend-general_height + }) + } + // Counters + general_height += line_height; + previous_line = line_number; + }); +} + +$(window).resize(function(){ + // Rebuild scroll markers after window high changing + coverage.resize_scroll_markers() +});
\ No newline at end of file |