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(""+msg+"");
}
}
- 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(""+msg+"");
}
}
- 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 = $("