From 229853e46fdf3c2a0ebecc29027f800481d0ffa3 Mon Sep 17 00:00:00 2001
From: "john.j.camilleri" <john.j.camilleri@chalmers.se>
Date: Tue, 29 Jan 2013 11:05:26 +0000
Subject: [PATCH] RGL browser: move help button, re-add synopsis link

---
 lib/doc/browse/index.html |  6 +++++-
 lib/doc/browse/script.js  | 18 +++++-------------
 lib/doc/browse/style.css  |  6 +++++-
 3 files changed, 15 insertions(+), 15 deletions(-)
diff --git a/lib/doc/browse/index.html b/lib/doc/browse/index.html
index 4faa70fb4..4d4eaa832 100644
--- a/lib/doc/browse/index.html
+++ b/lib/doc/browse/index.html
@@ -13,6 +13,8 @@
 <body>
   <header>
     <h1>RGL Source Browser</h1>
+    <a class="tab help" href="#help">Help</a>
+    <a href="http://www.grammaticalframework.org/lib/doc/synopsis.html" target="_blank">Synopsis...</a>
   </header>
   <div id="loading">
     <img src="ajax-loader.gif" /> Loading...
@@ -25,6 +27,8 @@
     <div class="pane right">
       <div id="tabbar">
         Module: <span id="module_name">...</span>
+        <a class="tab scope" href="#scope">scope</a>
+        <a class="tab code" href="#code">code</a>
       </div>
       <div id="scope" class="panel scope maxheight">
         <div id="scope_controls">
@@ -93,7 +97,7 @@
     <br style="clear:both" />
   </div>
   <footer id="footer">
-  John J. Camilleri<br/><em>Updated 2012-07-11</em>
+  John J. Camilleri<br/><em>Updated 2013-01-29</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>
diff --git a/lib/doc/browse/script.js b/lib/doc/browse/script.js
index c33d86893..edc49fc95 100644
--- a/lib/doc/browse/script.js
+++ b/lib/doc/browse/script.js
@@ -177,19 +177,11 @@ $(document).ready(function() {
         }
     });
 
-    // Initialize the panels & tabs
-    $(".panel").each(function(a,b){
-        $("<a>")
-            .addClass('tab')
-            .addClass($(b).attr('id'))
-            .attr('href', '#'+$(b).attr('id'))
-            .html($(b).attr('id'))
-            .click(function(){
-                showPanel(b);
-                return false;
-            })
-//            .appendTo("#tabbar")
-            .insertAfter("#tabbar *:last-child")
+    // Initialize the panels, tabs
+    $("a.tab").click(function(){
+        var panel = $(this).attr("href");
+        showPanel(panel);
+        return false;
     });
     showPanel(".panel:first");
 
diff --git a/lib/doc/browse/style.css b/lib/doc/browse/style.css
index c39fffb38..41a6e9433 100644
--- a/lib/doc/browse/style.css
+++ b/lib/doc/browse/style.css
@@ -23,8 +23,12 @@ header {
   padding:10px;
 }
 header h1 {
-  margin:0;
+  margin:0 1em 0 0;
   font-size:1em;
+  display: inline-block;
+}
+header .tab {
+  font-size: 90%;
 }
 div[role='main'] { 
   overflow:hidden;
