marks near the scroll

1 files changed, 73 insertions, 0 deletions

diff --git a/coverage/htmlfiles/coverage_html.js b/coverage/htmlfiles/coverage_html.js
index bd6a8753..fe126360 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'>&nbsp;</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