From 87e812455f373d250ccf00c1dfcfb2e3a4a8c97b Mon Sep 17 00:00:00 2001
From: "john.j.camilleri" <john.j.camilleri@chalmers.se>
Date: Tue, 15 May 2012 12:08:18 +0000
Subject: [PATCH] RGL Browser updates

- Better layout
- Jump to defition
- Syntax highlighting, line numbers
---
 lib/doc/browse/build-tags.sh |   3 +-
 lib/doc/browse/index.html    |  17 ++++--
 lib/doc/browse/index.json    |   1 +
 lib/doc/browse/script.js     | 104 ++++++++++++++++++++++++-----------
 lib/doc/browse/style.css     |  51 ++++++++++++++---
 5 files changed, 129 insertions(+), 47 deletions(-)
diff --git a/lib/doc/browse/build-tags.sh b/lib/doc/browse/build-tags.sh
index 7ad23068e..1c6998c41 100644
--- a/lib/doc/browse/build-tags.sh
+++ b/lib/doc/browse/build-tags.sh
@@ -9,7 +9,6 @@ dir=`pwd`
 basedir=${dir}/../../src
 tagsdir=${dir}/tags
 index=${dir}/index.json
-removeprefix="/home/john/repositories/GF"
 ignore="demo old-demo tmp"
 
 # Function for testing array membership
@@ -45,6 +44,6 @@ echo "  \"\":{}\n}\n}" >> $index
 # Replace all URLs
 echo "Replacing URLs"
 cd $tagsdir
-sed -i "s|${removeprefix}||g" *.gf-tags
+sed -ir "s|\S+?/lib/|/lib/|g" *.gf-tags
 
 exit 0
diff --git a/lib/doc/browse/index.html b/lib/doc/browse/index.html
index 582347a91..7fc5b74b1 100644
--- a/lib/doc/browse/index.html
+++ b/lib/doc/browse/index.html
@@ -8,11 +8,12 @@
   <meta name="viewport" content="width=device-width">
   <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-own.css">
 </head>
 <body>
   <header>
     <h1>GF RGL Browser</h1>
-    <p style="font-style:italic;margin-top:-0.5em;">Updated 2012-05-14</p>
+    <p style="font-style:italic;margin-top:-0.5em;">Updated 2012-05-15</p>
   </header>
   <div role="main">
     <div class="pane left">
@@ -28,14 +29,16 @@
       </div>
       <div id="scope" class="panel scope">
         <input type="text" id="search" />
+        &nbsp;<span id="scope_count">0</span> items&nbsp;
         <input type="submit" id="submit" value="Filter" />
         <input type="reset" id="clear" value="Clear" />
         <input type="checkbox" id="case_sensitive" checked="checked" />
         <label for="case_sensitive">Case sensitive?</label>
-        <div><span id="scope_count">0</span> items</div>
-        <dl id="scope_list"></dl>
+        <table id="scope_list"></table>
+      </div>
+      <div id="code" class="panel code">
+        <pre class="prettyprint lang-hs linenums"></pre>
       </div>
-      <div id="code" class="panel code"></div>
       <div id="help" class="panel help">
 
         <h3>Understanding the scope information</h3>
@@ -72,9 +75,10 @@
 
         <h3>Known issues and To-do</h3>
         <ul>
+          <li>Some way of browsing just the API</li>
+          <li>Some visual cue for </li>
           <li>The page sometimes stalls when handling large files (in particular the dictionary modules)</li>
-          <li>Jump directly to line in file</li>
-          <li>Line numbers and syntax highlighting for source code would be cool</li>
+          <li>Syntax highlighting is using a Haskell default, could cusomtise for GF</li>
         </ul>
       </div>
     </div>
@@ -84,6 +88,7 @@
     <p><em>John J. Camilleri, 2012</em></p>
   </footer>
   <script src="http://ajax.googleapis.com/ajax/libs/jquery/1.7.2/jquery.min.js"></script>
+  <script src="google-code-prettify/prettify.js"></script>
   <script src="script.js"></script>
 </body>
 </html>
\ No newline at end of file
diff --git a/lib/doc/browse/index.json b/lib/doc/browse/index.json
index c57196167..02999d2d7 100644
--- a/lib/doc/browse/index.json
+++ b/lib/doc/browse/index.json
@@ -1,4 +1,5 @@
 {
+"urlprefix": "/GF",
 "languages": {
   "abstract": [
     "Backward",
diff --git a/lib/doc/browse/script.js b/lib/doc/browse/script.js
index 707247072..0a6dd9180 100644
--- a/lib/doc/browse/script.js
+++ b/lib/doc/browse/script.js
@@ -4,9 +4,6 @@
 */
 $(document).ready(function() {
 
-//    var urlPrefix = "/GF"; // local
-    var urlPrefix = ""; // live
-
     var loading = function(b){
         if (b)
             $("#loading").show();
@@ -14,18 +11,47 @@ $(document).ready(function() {
             $("#loading").hide();
     }
 
-    var scrollToTop = function(){
-        $("html, body").animate({ scrollTop: 0 }, "slow");
+    var scrollToY = function(y, callback){
+        $("html, body").animate({ scrollTop: y }, "slow", callback);
+    }
+    var scrollToTop = function() {
+        scrollToY(0);
+    }
+    var scrollToCodeLine = function(lineNo) {
+        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 = obj.offset().top - 20;
+            scrollToY(y, function(){
+                highlight(obj);
+            });
+        });
+    }
+    var highlight = function(obj) {
+        obj.css('background-color', "yellow");
+        setTimeout(function(){
+            obj.css('background-color', "");
+        }, 1500);
+    }
+
+    var clearCode = function(code) {
+        $('#code pre').empty();
+    }
+    var setCode = function(code) {
+        $('#code pre').html(code);
+        prettyPrint();
     }
 
     var current_language = undefined;
+    var urlPrefix = "";
     var index;
     $.ajax({
         url: "index.json",
         dataType: "json",
         type: "GET",
-        success: function(data){
+        success: function(data) {
             index = data;
+            urlPrefix = data['urlprefix'];
 
             // Initialize the language list
             var lang_select = $("<select>")
@@ -77,9 +103,10 @@ $(document).ready(function() {
     };
 
     // Initialize the panels & tabs
-    var showPanel = function(obj){
+    // obj can be just a plain selector or a jQuery object
+    var showPanel = function(obj, callback){
         $(".panel").hide();
-        $(obj).show(); // obj can be just a plain selector or a jQuery object
+        $(obj).show(0, callback);
     }
     $(".panel").each(function(a,b){
         $("<a>")
@@ -92,7 +119,7 @@ $(document).ready(function() {
                 return false;
             })
             .insertBefore("#loading");
-    });
+   });
     showPanel(".panel:first");
 
     var setTitle = function(s){
@@ -100,14 +127,14 @@ $(document).ready(function() {
     }
 
     var updateScopeCount = function(){
-        $('#scope_count').text( $("#scope_list dt:visible").length );
+        $('#scope_count').text( $("#scope_list tr:visible").length );
     }
 
     // Load both scope & source for a file
-    var loadFile = function(lang, module){
+    var loadFile = function(lang, module, lineNo){
         setTitle(lang+"/"+module);
         loadTagsFile(module);
-        loadSourceFile(lang, module)
+        loadSourceFile(lang, module, lineNo)
     }
 
     // Load a tags file
@@ -121,18 +148,25 @@ $(document).ready(function() {
             type: "GET",
             dataType: "text",
             success: function(data){
-                data = data.replace(/^(\S+)\s+(.+)$/gm, '<dt name="$1">$1</dt><dd name="$1">$2</dd>');
-                // data = data.replace(/^(\S+)\s(\S+)\s(\S+)(.+)?$/gm, function(a,b,c,d,e){
-                //     return '<tr name="'+b+'"><th>'+b+'</th><td>'+c+'</td><td>'+d+'</td><td>'+e+'</td></tr>'
-                // });
-                data = data.replace(/\s(\/lib\/\S+?\.gf(-tags)?)/gm, '<a href="$1">$1</a>');
+                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 anchor = '<a href="'+s[2]+'">'+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 anchor = '<a href="'+s[0]+'">'+s[0]+'</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>'
+                    }
+                });
                 $('#scope_list').html(data);
                 $('#scope_list a').click(function(){
                     var href = $(this).attr('href');
-                    var m = href.match(/([^\/]+)\/([^\/]+)\.(gf(-tags)?)$/);
+                    var m = href.match(/([^\/]+)\/([^\/]+)\.(gf(-tags)?)(:\d+)?/);
                     if (m[3]=="gf") {
                         // Load both tags and source
-                        loadFile(m[1], m[2]);
+                        var lineNo = m[5].slice(1);
+                        loadFile(m[1], m[2], lineNo);
                     } else if (m[3]=="gf-tags") {
                         // Try and determine the language from the contents
                         checkSourceFile({
@@ -140,16 +174,17 @@ $(document).ready(function() {
                             module: m[2],
                             onsuccess: function(){
                                 loadFile(current_language, m[2]);
+                                scrollToTop();
                             },
                             onerror: function(){
                                 // Load just tags (we don't know source)
                                 setTitle(m[2]+" (scope only)");
-                                $('#code').empty();
+                                clearCode();
                                 loadTagsFile(m[2]);
+                                scrollToTop();
                             }
                         });
                     }
-                    scrollToTop();
                     return false;
                 });
                 updateScopeCount();
@@ -173,19 +208,22 @@ $(document).ready(function() {
     }
 
     // Load a source module
-    var loadSourceFile = function(lang, module) {
-        $('#code').empty();
+    var loadSourceFile = function(lang, module, lineNo) {
+        clearCode();
         loading(true);
         $.ajax({
             url: urlPrefix + "/lib/src/"+lang+"/"+module+".gf",
             type: "GET",
             dataType: "text",
             success: function(data){
-                $('#code').html(data);
+                setCode(data);
                 loading(false);
+                if (lineNo) {
+                    scrollToCodeLine(lineNo);
+                }
             },
             error: function(data){
-                $('#code').html("<em>No code available</em>");
+                setCode("<em>No code available</em>");
                 loading(false);
             }
         });
@@ -208,11 +246,10 @@ $(document).ready(function() {
         loading(true);
         try {
             if (s) {
-                $("#scope_list").children(     ":match(\""+s+"\")").show();
-                $("#scope_list").children(":not(:match(\""+s+"\"))").hide();
-                //$("#scope_list tr:not(:match(\""+s+"\"))").hide();
+                $("#scope_list tr:match(\""+s+"\")").show();
+                $("#scope_list tr:not(:match(\""+s+"\"))").hide();
             } else {
-                $("#scope_list").children().show();
+                $("#scope_list tr").show();
             }
         } catch (error) {
             alert(error.message);
@@ -221,14 +258,19 @@ $(document).ready(function() {
         loading(false);
     }
 
-//    $("#search").keyup(runfilter);
+    // Instant results
+    $("#search").keyup(runfilter);
+    $("#submit").hide();
+
+    // Filter & clear buttons
+    // $("#submit").click(runfilter);
+
     $("#search").keypress(function(e){
         var code = (e.keyCode ? e.keyCode : e.which);
         if(code == 13) { // Enter
             runfilter();
         }        
     });
-    $("#submit").click(runfilter);
     $("#clear").click(function(){
         $("#search").val('');
         runfilter();
diff --git a/lib/doc/browse/style.css b/lib/doc/browse/style.css
index ccca8f6db..ab8117b94 100644
--- a/lib/doc/browse/style.css
+++ b/lib/doc/browse/style.css
@@ -24,6 +24,10 @@ div[role='main']
 { 
   margin-left:170px;
  }
+.panel
+{
+  padding:1em;
+  }
 .button
 {
   cursor:pointer;
@@ -63,8 +67,15 @@ div[role='main']
   }
 #loading
 { 
-  display:inline-block;
-  color:#666;
+  position: fixed;
+  top: 1em;
+  right: 1em;
+  white-space: nowrap;
+  padding: 0.5em 1em;
+  border: 1px solid #F0C36D;
+  background: #F9EDBE;
+  color: black;
+  vertical-align: middle;
  }
 .scope
 { 
@@ -91,16 +102,40 @@ input#search
 #scope_list
 {
   font-family:monospace;
+  width:100%;
+  margin-top:1em;
   }
-#scope_list dt
+#scope_list tr:hover
 {
-  float:left;
+  background:#eee;
   }
-#code
+#scope_list tr.indir
 {
-  font-family:monospace;
-  white-space:pre;
-  padding: 1em;
+  font-style:italic;
+  }
+#scope_list tr.local td:nth-child(2)
+{
+  font-weight:bold;
+  }
+#scope_list th
+{
+  text-align:left;
+  }
+#scope_list th, #scope_list td
+{
+  padding:0.4em;
+  border: 1px solid #aaa;
+  background:none;
+  white-space:nowrap;
+  }
+#scope_list td:nth-child(6)
+{
+  white-space:normal;
+  }
+#code pre
+{
+  margin:0;
+  color:#000;
   }
 dt
 { 
