RGL Browser: updates

lib/doc/browse/index.html

@@ -6,7 +6,7 @@
   <title>RGL Source Browser</title>
   <meta name="description" content="">
   <meta name="viewport" content="width=device-width">
-  <link rel="shortcut icon" href="http://cdn.dustball.com/book_next.png" type="image/png">
+  <link rel="shortcut icon" href="icon.png" type="image/png">
   <link rel="stylesheet" href="http://www.grammaticalframework.org/css/style.css">
   <link rel="stylesheet" href="style.css">
   <link rel="stylesheet" href="google-code-prettify/prettify-gf.css">
@@ -16,7 +16,7 @@
     <h1>RGL Source Browser</h1>
   </header>
   <div id="loading">
-    <img src="ajax-loader.gif" /> loading...
+    <img src="ajax-loader.gif" /> Loading...
   </div>
   <div role="main">
     <div class="pane left">
@@ -29,13 +29,15 @@
         <a href="http://www.grammaticalframework.org/lib/doc/synopsis.html" title="RGL Synopsis">Synopsis...</a>
       </div>
       <div id="scope" class="panel scope maxheight">
-        <input type="text" id="search" />
+        <div id="scope_controls">
-        &nbsp;<span id="scope_count">0</span> items&nbsp;
+          <input type="text" id="search" />
-        <input type="submit" id="submit" value="Filter" />
+          &nbsp;<span id="scope_count">0</span> items&nbsp;
-        <input type="reset" id="clear" value="Clear" />
+          <input type="submit" id="submit" value="Filter" />
-        <input type="checkbox" id="case_sensitive" checked="checked" /><label for="case_sensitive">Case sensitive?</label>
+          <input type="reset" id="clear" value="Clear" />
-        <input type="radio" name="show" id="show_all" checked="checked" /><label for="show_all">Show all</label>
+          <input type="checkbox" id="case_sensitive" checked="checked" /><label for="case_sensitive">Case sensitive?</label>
-        <input type="radio" name="show" id="show_local" /><label for="show_local">Local only</label>
+          <input type="radio" name="show" id="show_all" checked="checked" /><label for="show_all">Show all</label>
+          <input type="radio" name="show" id="show_local" /><label for="show_local">Local only</label>
+        </div>
         <div class="maxheight scroll-y">
           <table id="scope_list"></table>
         </div>
@@ -46,10 +48,12 @@
       <div id="help" class="panel help maxheight">
       <div class="maxheight scroll-y">
 
+        <h3>About</h3>
+        <p>A basic tool for looking through scopes and quickly jumping to code within GF's resource grammar library (RGL), created out of necessity. All feedback is welcome.</p>
+
         <h3>Understanding the scope information</h3>
         <p>The scope information shown by this tool is basically the output of running GF with the <code>--tags</code> flag. This lists all the functions visible in the scope of a module, one per line. Each line can have two possible forms:</p>
 
-
         <h4>1. Local functions</h4>
         <pre>mkPrep	oper-type	/lib/src/english/ParadigmsEng.gf:204	Str -> {s : Str; lock_Prep : {}}</pre>
         <p>For locally defined functions, the second column <code>oper-type</code> indicates the judgement type, followed by the location in the souce file and its type information.</p>
@@ -75,10 +79,12 @@
           <dt><code>scandinavian</code></dt><dd>Used by Danish, Norwegian, Swedish</dd>
         </dl>
         
-        <h3>About</h3>
+        <h3>Issues</h3>
-        <p>A basic tool for looking up module scopes and quickly looking at module sources, created out of necessity. It is experimental and is known to hang when handling large files. All feedback is welcome.</p>
 
-        <h3>Known issues and To-do</h3>
+        <h4>Something is missing or out of date</h4>
+        <p>All the scoping information shown is not read directly from the RGL on-demand. There is an in-between processing stage which must be run, so if something seems out of date just let me know and I can udpate things manually.</p>
+
+        <h4>To-Do</h4>
         <ul>
           <li>Some way of browsing just the API</li>
           <li>The page sometimes stalls when handling large files (in particular the dictionary modules)</li>
@@ -89,7 +95,7 @@
     <br style="clear:both" />
   </div>
   <footer id="footer">
-  John J. Camilleri. <em>Updated 2012-05-25.</em>
+  John J. Camilleri<br/><em>Updated 2012-07-11</em>
   </footer>
   <script src="http://ajax.googleapis.com/ajax/libs/jquery/1.7.2/jquery.min.js"></script>
   <script src="jquery.history.min.js"></script>
@@ -97,4 +103,4 @@
   <script src="google-code-prettify/lang-gf.js"></script>
   <script src="script.js"></script>
 </body>
-</html>
+</html>

lib/doc/browse/script.js

@@ -4,14 +4,60 @@
 */
 $(document).ready(function() {
 
-    var loadCount = 0;
+    // ===== State information =====
+
+    state = {
+        index: undefined,
+        lookup: {},
+        loadCount: 0,
+        language: undefined, // lang of drop-down
+        current: { // current file
+            language: undefined,
+            module: undefined,
+            set: function(lang, module) {
+                state.current.language = lang;
+                state.current.module = module;
+            },
+            equals: function(a, b) {
+                if (!b)
+                    return (a == state.current.module);
+                else
+                    return (a == state.current.language) && (b == state.current.module);
+            }
+        },
+        title: "RGL Source Browser",
+        urlPrefix: "/",
+        defaultLangs: ['abstract','api','common','prelude']
+    } ;
+
+    var lookupModuleLanguage = function(module) {
+        var l = state.lookup[module];
+        if (l==undefined || l.length==0)
+            return null;
+        else if (l.length==1)
+            return l[0];
+        else {
+            for (i in l) {
+                if ($.inArray(l[i], state.defaultLangs))
+                    return l[i];
+            }
+            return l[0]; // no preferred default, just return first...
+        }
+    }
+    var lookupAllModuleLanguages = function(module) {
+        return state.lookup[module];
+    }
+
+
+    // ===== Utility/UI functions =====
+
     var showLoading = function(){
-        loadCount++;
+        state.loadCount++;
         $("#loading").show();
     }
     var hideLoading = function(){
-        loadCount = Math.max(loadCount-1, 0);
+        state.loadCount = Math.max(state.loadCount-1, 0);
-        if (loadCount == 0)
+        if (state.loadCount == 0)
             $("#loading").hide();
     }
 
@@ -55,17 +101,57 @@ $(document).ready(function() {
         $('#code pre').html(code);
         prettyPrint();
     }
+    var updateScopeCount = function(){
+        $('#scope_count').text( $("#scope_list tr:visible").length );
+    }
 
-    var current_language = undefined;
+    var setLanguage = function(lang){
-    var urlPrefix = "/";
+        state.language = lang;
-    var index;
+        $("#languages select").val(lang);
+        initModules(lang);
+    }
+
+    // obj can be just a plain selector or a jQuery object
+    var showPanel = function(obj, callback){
+        showLoading();
+        setTimeout(function(){
+            $(".panel:visible").hide();
+            $(obj).show(0, callback);
+            recalculateHeights();
+            updateScopeCount();
+            hideLoading();
+        }, 500); // this ensures the loading displays
+    }
+    var getPanel = function() {
+        return $('.panel:visible').first();
+    }
+
+    var setTitle = function(s){
+        $('#tabbar h2').html(s);
+        $('title').html(state.title + ": " + s);
+    }
+
+
+    // ===== Initialization =====
+
+    // Load the index file and populate language & module lists
     $.ajax({
         url: "index.json",
         dataType: "json",
         type: "GET",
         success: function(data) {
-            index = data;
+            state.index = data;
-            if (data['urlprefix']) urlPrefix = data['urlprefix'];
+            if (data['urlprefix']) state.urlPrefix = data['urlprefix'];
+
+            // Build language lookup index
+            for (var lang in data['languages']) {
+                for (var i in data['languages'][lang]) {
+                    var module = data['languages'][lang][i];
+                    if (!module) continue;
+                    if (!state.lookup[module]) state.lookup[module] = [];
+                    state.lookup[module].push(lang);
+                }
+            }
 
             // Initialize the language list
             var lang_select = $("<select>")
@@ -75,7 +161,7 @@ $(document).ready(function() {
                 })
                 .appendTo("#languages")
             var language_list = data['languages'];
-            for (i in language_list) {
+            for (var i in language_list) {
                 if (!i) continue;
                 var lang = i;
                 $('<option>')
@@ -91,41 +177,7 @@ $(document).ready(function() {
         }
     });
 
-    var setLanguage = function(lang){
-        current_language = lang;
-        $("#languages select").val(lang);
-        initModules(lang);
-    }
-
-    // Initialize the module list
-    var initModules = function(lang){
-        index['languages'][lang] = index['languages'][lang].sort();
-        $("#modules").empty();
-        for (i in index['languages'][lang]) {
-            var module = index['languages'][lang][i];
-            if (!module) continue;
-            $('<a>')
-                .html(module)
-                .addClass('button')
-                .attr('href', "#"+lang+"/"+module+".gf")
-                .appendTo("#modules");
-        }
-    };
-
     // Initialize the panels & tabs
-    // obj can be just a plain selector or a jQuery object
-    var showPanel = function(obj, callback){
-        showLoading();
-        setTimeout(function(){
-            $(".panel:visible").hide();
-            $(obj).show(0, callback);
-            recalculateHeights();
-            hideLoading();
-        }, 500); // this ensures the loading displays
-    }
-    var getPanel = function() {
-        return $('.panel:visible').first();
-    }
     $(".panel").each(function(a,b){
         $("<a>")
             .addClass('tab')
@@ -138,22 +190,60 @@ $(document).ready(function() {
             })
 //            .appendTo("#tabbar")
             .insertBefore("#tabbar *:last-child")
-   });
+    });
     showPanel(".panel:first");
 
-    var setTitle = function(s){
-        $('#tabbar h2').html(s);
-    }
 
-    var updateScopeCount = function(){
+    // ===== URL history =====
-        $('#scope_count').text( $("#scope_list tr:visible").length );
+
-    }
+    $.History.bind(function(hash){
+        var s = hash.split("/");
+        var lang = s[0];
+        var module = stripExt(s[1]);
+        var parseLineNo = s[1].match(/:(\d+)(-(\d+))?$/);
+
+        if (state.current.equals(lang, module)) {
+            if (parseLineNo) {
+                scrollToCodeLine(parseInt(parseLineNo[1]));
+            }
+            // else there's nothing to do!
+        } else {
+            if (parseLineNo != undefined)
+                loadFile(lang, module, parseInt(parseLineNo[1]));
+            else
+                loadFile(lang, module);
+        }
+    });
+
+    var stripExt = function(s) {
+        var i = s.lastIndexOf('.');
+        return (i>-1) ? s.substr(0, i) : s;
+    };
+
+
+    // ===== Loading functionality =====
+
+    // Initialize the module list
+    var initModules = function(lang){
+        state.index['languages'][lang] = state.index['languages'][lang].sort();
+        $("#modules").empty();
+        for (var i in state.index['languages'][lang]) {
+            var module = state.index['languages'][lang][i];
+            if (!module) continue;
+            $('<a>')
+                .html(module)
+                .addClass('button')
+                .attr('href', "#"+lang+"/"+module+".gf")
+                .appendTo("#modules");
+        }
+    };
 
     // Load both scope & source for a file
     var loadFile = function(lang, module, lineNo){
         setTitle(lang+"/"+module);
+        state.current.set(lang, module);
         loadTagsFile(module);
-        loadSourceFile(lang, module, lineNo)
+        loadSourceFile(lang, module, lineNo);
     }
 
     // Load a tags file
@@ -168,19 +258,21 @@ $(document).ready(function() {
                 data = data.replace(/^(\S+)\s(\S+)\s(.+)?$/gm, function(a,b,c,d){
                     var s = d.split("\t");
                     if (c == "indir") {
-                        var name = s[2].slice(s[2].lastIndexOf('/')+1);
+                        var module = s[2].substring(s[2].lastIndexOf('/')+1, s[2].lastIndexOf('.'));
-                        var url = "#"+name;
+                        var lang = lookupModuleLanguage(module);
+                        var name =    lang+"/"+module;
+                        var url = "#"+lang+"/"+module;
                         var anchor = '<a href="'+url+'">'+name+'</a>';
                         return '<tr class="indir" name="'+b+'"><th>'+b+'</th><td>'+c+'</td><td>'+s[0]+'</td><td>'+s[1]+'</td><td>'+anchor+'</td><td></td></tr>'
                     } else {
                         var bits = s[0].split("/"); // ["lib", "src", "english", "AdjectiveEng.gf:43-46"]
+                        var name =    bits[3]+"/"+bits[4];
                         var url = "#"+bits[3]+"/"+bits[4];
-                        var anchor = '<a href="'+url+'">'+s[0]+'</a>';
+                        var anchor = '<a href="'+url+'">'+name+'</a>';
                         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);
-                updateScopeCount();
                 runFilter();
                 hideLoading();
             },
@@ -191,22 +283,12 @@ $(document).ready(function() {
         });
     }
 
-    // Just get the HTTP headers to see if a file exists
-    var checkSourceFile = function(args) {
-        $.ajax({
-            url: urlPrefix + "lib/src/"+args.lang+"/"+args.module+".gf",
-            type: "HEAD",
-            success: args.onsuccess,
-            error: args.onerror
-        });    
-    }
-
     // Load a source module
     var loadSourceFile = function(lang, module, lineNo) {
         clearCode();
         showLoading();
         $.ajax({
-            url: urlPrefix + "lib/src/"+lang+"/"+module+".gf",
+            url: state.urlPrefix + "lib/src/"+lang+"/"+module+".gf",
             type: "GET",
             dataType: "text",
             success: function(data, status, xhr){
@@ -223,6 +305,9 @@ $(document).ready(function() {
         });
     }
 
+
+    // ===== Filtering of scope info =====
+
     // Custom selector
     $.expr[':'].match = function(a,b,c) {
         var obj = $(a);
@@ -237,7 +322,7 @@ $(document).ready(function() {
     };
 
     var runFilter = function() {
-        showLoading()
+        showLoading();
         var s = $("#search").val();
         try {
             if (s) {
@@ -286,41 +371,8 @@ $(document).ready(function() {
     $("#show_all").change(runFilter);
     $("#show_local").change(runFilter);
 
-    // ===== URL history =====
-    $.History.bind(function(state){
-        var s = state.split("/");
-        if (s[0].match(/\.gf-tags$/)) {
-            var module = stripExt(s[0]);
-            checkSourceFile({
-                lang: current_language,
-                module: module,
-                onsuccess: function(){
-                    $.History.go(current_language+"/"+module);
-                },
-                onerror: function(){
-                    // Load just tags (we don't know source)
-                    setTitle(module+" (scope only)");
-                    clearCode();
-                    loadTagsFile(module);
-                    scrollToTop();
-                }
-            });
-        } else {
-            var lang = s[0];
-            var module = stripExt(s[1]);
-            var parseLineNo = s[1].match(/:(\d+)(-(\d+))?$/);
-            if (parseLineNo != undefined)
-                loadFile(lang, module, parseInt(parseLineNo[1]));
-            else
-                loadFile(lang, module);
-        }
-    });
 
-    var stripExt = function(s) {
+    // ===== Window resizing stuff =====
-        return s.substr(0, s.lastIndexOf('.'));
-    };
-
-    // ===== Resizing stuff =====
 
     // refer: http://paulirish.com/2009/throttled-smartresize-jquery-event-handler/
     (function($,sr){
@@ -354,7 +406,7 @@ $(document).ready(function() {
     });
 
     var recalculateHeights = function() {
-        $('body').height( $(window).height()-85); //80 was just found empirically
+        $('body').height( $(window).height()-60); // just found empirically
         $('.maxheight').each(function(){
             var obj = $(this);
             var parent = obj.parent();

lib/doc/browse/style.css

@@ -26,6 +26,8 @@ div[role='main']
 { 
   width:170px;
   float:left;
+  background:#ddd;
+  padding:0.2em;
  }
 .pane.right
 { 
@@ -47,11 +49,8 @@ div[role='main']
  }
 #language_select
 { 
-  font-size:1.1em;
+  font-size:1em;
-  }
+  width:100%;
-#languages
-{ 
-  margin:0.5em 0;
   }
 #modules a
 { 
@@ -88,14 +87,15 @@ div[role='main']
 #loading
 { 
   position: fixed;
-  top: 1em;
+  top: 5px;
-  right: 1em;
+  left: 50%;
   white-space: nowrap;
   padding: 0.5em 1em;
   border: 1px solid #F0C36D;
   background: #F9EDBE;
-  color: black;
+  color: #222;
-  vertical-align: middle;
+  vertical-align: top;
+  font-family: sans-serif;
  }
 .scope
 { 
@@ -124,6 +124,11 @@ input#search
 {
   padding: 1em;
   }
+#scope_controls
+{ 
+  border-bottom: 1px solid #CCC;
+  padding-bottom: 0.5em;
+  }
 #scope_list
 {
   font-family:monospace;
@@ -171,9 +176,11 @@ dt
   }
 footer
 { 
-  padding: 0.4em;
+  padding:0.5em;
   color:#333;
-  text-align:right;
-  border-top:1px solid #ccc;
   font-size:0.9em;
+  text-align:right;
+  position:fixed;
+  top:0;
+  right:0;
   }