mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-04-09 04:59:31 -06:00
RGL Browser: fix issue with jumping to code locations
This commit is contained in:
@@ -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();
|
||||
});
|
||||
};
|
||||
|
||||
@@ -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;
|
||||
|
||||
Reference in New Issue
Block a user