From 4512d6f1979fbb0feb7feab478a910f3c992e3f3 Mon Sep 17 00:00:00 2001
From: "john.j.camilleri" <john.j.camilleri@chalmers.se>
Date: Tue, 23 Jul 2013 14:42:59 +0000
Subject: [PATCH] RGL Browser: fix issue with jumping to code locations

---
 lib/doc/browse/script.js | 167 ++++++++++++++++++++-------------------
 lib/doc/browse/style.css |   3 -
 2 files changed, 85 insertions(+), 85 deletions(-)

diff --git a/lib/doc/browse/script.js b/lib/doc/browse/script.js
index f5834302f..17e9251ca 100644
--- a/lib/doc/browse/script.js
+++ b/lib/doc/browse/script.js
@@ -1,6 +1,6 @@
 /*
   GF RGL Browser
-  John J. Camilleri, 2012
+  John J. Camilleri, 2013
 */
 
 var thing = null;
@@ -22,11 +22,11 @@ $(document).ready(function(){
 
         if (thing.state.current.equals(lang, module)) {
             if (parseLineNo) {
-                scrollToCodeLine(parseInt(parseLineNo[1]));
+                thing.scrollToCodeLine(parseInt(parseLineNo[1]));
             }
             // else there's nothing to do!
         } else {
-            if (parseLineNo != null)
+            if (parseLineNo != undefined)
                 thing.loadFile(lang, module, parseInt(parseLineNo[1]));
             else
                 thing.loadFile(lang, module);
@@ -63,7 +63,7 @@ function Thing() {
         defaultLangs: ['abstract','api','common','prelude']
     } ;
 
-    var lookupModuleLanguage = function(module) {
+    this.lookupModuleLanguage = function(module) {
         var l = t.state.lookup[module];
         if (l==undefined || l.length==0)
             return null;
@@ -77,90 +77,92 @@ function Thing() {
             return l[0]; // no preferred default, just return first...
         }
     }
-    var lookupAllModuleLanguages = function(module) {
+    this.lookupAllModuleLanguages = function(module) {
         return t.state.lookup[module];
     }
 
     // ===== Utility/UI functions =====
 
-    var showLoading = function(){
+    this.showLoading = function(){
         t.state.loadCount++;
         $("#loading").show();
     }
-    var hideLoading = function(){
+    this.hideLoading = function(){
         t.state.loadCount = Math.max(t.state.loadCount-1, 0);
         if (t.state.loadCount == 0)
             $("#loading").hide();
     }
 
-    var scrollToTop = function() {
+    this.scrollToTop = function() {
         $("html, body").animate({ scrollTop: 0 }, "slow");
     }
-    var scrollToCodeLine = function(lineNo) {
-        showPanel("#code", function() {
+    this.scrollToCodeLine = function(lineNo) {
+        t.showPanel("#code", function() {
             // Find exact line, using the classes generated by google prettify
-            var obj = $("#code pre li.L"+(lineNo%10)+":eq("+Math.floor(lineNo/10)+")").prev();
-            var y = Math.max(obj.offset().top - obj.parent().offset().top - 75, 0);
-            $("#code pre").animate({ scrollTop: y }, "slow", function(){
-                highlight(obj);
-            });
+            try {
+                var obj = $("#code pre li.L"+(lineNo%10)+":eq("+Math.floor(lineNo/10)+")").prev();
+                var y = Math.max(obj.offset().top - obj.parent().offset().top - 75, 0);
+                $("#code pre").animate({ scrollTop: y }, "slow", function(){
+                    t.highlight(obj);
+                });
+            } catch (e) {}
         });
     }
-    var highlight = function(obj) {
+    this.highlight = function(obj) {
         obj.css('background-color', "yellow");
         setTimeout(function(){
             obj.css('background-color', "");
         }, 1500);
     }
 
-    var clearScope = function(msg) {
+    this.clearScope = function(msg) {
         $('#scope #results').empty();
-        updateScopeCount();
+        t.updateScopeCount();
         if (msg) {
             $('#scope #results').html("<em>"+msg+"</em>");
         }
     }
-    var setScope = function(code) {
+    this.setScope = function(code) {
         $('#scope #results').html(code);
     }
-    var clearCode = function(msg) {
+    this.clearCode = function(msg) {
         $('#code pre').empty();
         if (msg) {
             $('#codes pre').html("<em>"+msg+"</em>");
         }
     }
-    var setCode = function(code) {
+    this.setCode = function(code) {
         $('#code pre').text(code);
         prettyPrint();
     }
-    var updateScopeCount = function(){
+    this.updateScopeCount = function(){
         $('#scope #count').text( $("#scope #results tr:visible").length );
     }
-    var updateAPICount = function(){
+    this.updateAPICount = function(){
         $('#api #count').text( $("#api #results tr:visible").length );
     }
 
-    var setLanguage = function(lang){
+    this.setLanguage = function(lang){
         t.state.language = lang;
         $("#languages select").val(lang);
-        initModules(lang);
+        t.initModules(lang);
     }
 
     // obj can be just a plain selector or a jQuery object
     this.showPanel = function(obj, callback){
-        showLoading();
+        t.showLoading();
         setTimeout(function(){
             $(".panel:visible").hide();
             $(obj).show(0, callback);
-            updateScopeCount();
-            hideLoading();
+            t.updateScopeCount();
+            t.hideLoading();
         }, 500); // this ensures the loading displays
     }
-    var getPanel = function() {
+    this.getPanel = function() {
         return $('.panel:visible').first();
     }
 
-    var setTitle = function(s){
+    this.setTitle = function(s){
         $('#module_name').html(s);
         $('title').html(t.state.title + ": " + s);
     }
@@ -199,7 +201,7 @@ function Thing() {
             var lang_select = $("<select>")
                 .attr('id', 'language_select')
                 .change(function(){
-                    setLanguage($(this).val());
+                    t.setLanguage($(this).val());
                 })
                 .appendTo("#languages")
             var language_list = data['languages'];
@@ -210,16 +212,16 @@ function Thing() {
                     .html(lang)
                     .appendTo(lang_select);
             }
-            setLanguage("english");
+            t.setLanguage("english");
 
             // Initialize API results
-            initAPI();
+            t.initAPI();
 
             // Done
-            hideLoading();
+            t.hideLoading();
         },
         error: function(){
-            hideLoading();
+            t.hideLoading();
             alert("Error getting index. Try reloading page, or just give up.");
         }
     });
@@ -228,7 +230,7 @@ function Thing() {
     // ===== Loading functionality =====
 
     // Initialize the module list
-    var initModules = function(lang){
+    this.initModules = function(lang){
         t.state.index['languages'][lang] = t.state.index['languages'][lang].sort();
         $("#modules").empty();
         for (var i in t.state.index['languages'][lang]) {
@@ -243,16 +245,16 @@ function Thing() {
 
     // Load both scope & source for a file
     this.loadFile = function(lang, module, lineNo){
-        setTitle(lang+"/"+module);
+        t.setTitle(lang+"/"+module);
         t.state.current.set(lang, module);
-        loadTagsFile(module);
-        loadSourceFile(lang, module, lineNo);
+        t.loadTagsFile(module);
+        t.loadSourceFile(lang, module, lineNo);
     }
 
     // Load a tags file
-    var loadTagsFile = function(module) {
-        clearScope();
-        showLoading();
+    this.loadTagsFile = function(module) {
+        t.clearScope();
+        t.showLoading();
         $.ajax({
             url: "tags/"+module+".gf-tags",
             type: "GET",
@@ -262,7 +264,7 @@ function Thing() {
                     var s = d.split("\t");
                     if (c == "indir") {
                         var module = s[2].substring(s[2].lastIndexOf('/')+1, s[2].lastIndexOf('.'));
-                        var lang = lookupModuleLanguage(module);
+                        var lang = t.lookupModuleLanguage(module);
                         var name =    lang+"/"+module;
                         var url = "#"+lang+"/"+module;
                         var anchor = '<a href="'+url+'">'+name+'</a>';
@@ -275,41 +277,41 @@ function Thing() {
                         return '<tr class="local" name="'+b+'"><th>'+b+'</th><td>'+c+'</td><td></td><td></td><td>'+anchor+'</td><td>'+s[1]+'</td></tr>'
                     }
                 });
-                setScope(data);
-                runFilter();
-                hideLoading();
+                t.setScope(data);
+                t.runFilter();
+                t.hideLoading();
             },
             error: function(data){
-                clearScope("No scope available");
-                hideLoading();
+                t.clearScope("No scope available");
+                t.hideLoading();
             },
         });
     }
 
     // Load a source module
-    var loadSourceFile = function(lang, module, lineNo) {
-        clearCode();
-        showLoading();
+    this.loadSourceFile = function(lang, module, lineNo) {
+        t.clearCode();
+        t.showLoading();
         $.ajax({
             url: t.state.urlPrefix + "lib/src/"+lang+"/"+module+".gf",
             type: "GET",
             dataType: "text",
             success: function(data, status, xhr){
-                setCode(data);
-                hideLoading();
+                t.setCode(data);
+                t.hideLoading();
                 if (lineNo) {
-                    scrollToCodeLine(lineNo);
+                    t.scrollToCodeLine(lineNo);
                 }
             },
             error: function(data){
-                clearCode("No code available");
-                hideLoading();
+                t.clearCode("No code available");
+                t.hideLoading();
             }
         });
     }
 
     // Which modules do we include for API?
-    var apiModules = [
+    this.apiModules = [
         // api
         "Constructors",
         // abstract
@@ -339,11 +341,11 @@ function Thing() {
         "Transfer",
         "Verb",
     ];
-    var initAPI = function() {
-        showLoading();
+    this.initAPI = function() {
+        t.showLoading();
         $('#api #results').empty();
-        for (var i in apiModules) {
-            var module = apiModules[i];
+        for (var i in t.apiModules) {
+            var module = t.apiModules[i];
             $.ajax({
                 url: "tags/"+module+".gf-tags",
                 type: "GET",
@@ -367,13 +369,14 @@ function Thing() {
                     $('#api #results').append($(data));
                     $("#api #results tr").removeClass('odd');
                     $("#api #results tr:odd").addClass('odd');
+                    $('#api #count').text( $("#api #results tr").length );
                 },
                 error: function(data){
                     console.log("Error loading tags file: " + module);
                 },
             });
         }
-        hideLoading();
+        t.hideLoading();
     }
 
 
@@ -392,8 +395,8 @@ function Thing() {
             return haystack.toLowerCase().indexOf(needle.toLowerCase())>=0;
     };
 
-    var runFilter = function() {
-        showLoading();
+    this.runFilter = function() {
+        t.showLoading();
         $("#scope #results tr").removeClass('odd');
         var s = $("#scope #search").val();
         try {
@@ -409,17 +412,17 @@ function Thing() {
         } catch (error) {
             alert(error.message);
         }
-        updateScopeCount();
+        t.updateScopeCount();
         $("#scope #results tr:visible:odd").addClass('odd');
-        hideLoading();
+        t.hideLoading();
     }
 
     // Instant results
-    var prevSearch = $("#scope #search").val();
+    this.prevSearch = $("#scope #search").val();
     $("#scope #search").keyup(function(){
         var s = $("#scope #search").val();
         if (s!=prevSearch) {
-            runFilter();
+            t.runFilter();
             prevSearch = s;
         }
     });
@@ -427,18 +430,18 @@ function Thing() {
     $("#scope #search").keypress(function(e){
         var code = (e.keyCode ? e.keyCode : e.which);
         if(code == 13) { // Enter
-            runFilter();
+            t.runFilter();
         }
     });
     $("#scope #clear").click(function(){
         $("#scope #search")
             .val('')
             .focus()
-        runFilter();
+        t.runFilter();
     });
-    $("#scope #case_sensitive").change(runFilter);
-    $("#scope #show_all").change(runFilter);
-    $("#scope #show_local").change(runFilter);
+    $("#scope #case_sensitive").change(t.runFilter);
+    $("#scope #show_all").change(t.runFilter);
+    $("#scope #show_local").change(t.runFilter);
 
     // ===== API search =====
 
@@ -456,8 +459,8 @@ function Thing() {
             return match_ident || match_type ;
     };
 
-    var runFilterAPI = function() {
-        showLoading();
+    this.runFilterAPI = function() {
+        t.showLoading();
         $("#api #results tr").removeClass('odd');
         var s = $("#api #search").val();
         try {
@@ -470,17 +473,17 @@ function Thing() {
         } catch (error) {
             alert(error.message);
         }
-        updateAPICount();
+        t.updateAPICount();
         $("#api #results tr:visible:odd").addClass('odd');
-        hideLoading();
+        t.hideLoading();
     }
 
     // Instant results
-    var prevAPISearch = $("#api #search").val();
+    this.prevAPISearch = $("#api #search").val();
     $("#api #search").keyup(function(){
         var s = $("#api #search").val();
         if (s!=prevAPISearch) {
-            runFilterAPI();
+            t.runFilterAPI();
             prevAPISearch = s;
         }
     });
@@ -488,13 +491,13 @@ function Thing() {
     $("#api #search").keypress(function(e){
         var code = (e.keyCode ? e.keyCode : e.which);
         if(code == 13) { // Enter
-            runFilterAPI();
+            t.runFilterAPI();
         }
     });
     $("#api #clear").click(function(){
         $("#api #search")
             .val('')
-            .focus()
-        runFilterAPI();
+            .focus();
+        t.runFilterAPI();
     });
 };
diff --git a/lib/doc/browse/style.css b/lib/doc/browse/style.css
index e42fbf39e..eec79806a 100644
--- a/lib/doc/browse/style.css
+++ b/lib/doc/browse/style.css
@@ -125,9 +125,6 @@ input#search {
   margin-top:1em;
   border-collapse: collapse;
 }
-#results tr:hover {
-  background:#f9f9f9;
-}
 /* this is set in code */
 #results tr.odd {
   background:ghostwhite;