minibar: add a button to get detailed grammar info

After pressing the "i" button to view grammar info, there is now a
"More info" button to get more detailed information about all categories and
functions in the grammar.

src/www/minibar/about.html

@@ -217,11 +217,15 @@ Some implementation details:
  <li>[Added 2012-11-23] Added support for switching back and forth between the
      minibar and the new syntax tree editor. The default configuration in
      <code>minibar_online.js</code> shows how to enable it.
+  <li>[Added 2012-11-29] After pressing the <strong>i</strong> button to view
+      grammar info, there is now a <strong>More info</strong> button to get
+      more detailed information about all categories and functions in the
+      grammar.
 </ul>
 
 <hr>
 <div class=modtime><small>
-<!-- hhmts start -->Last modified: Thu Nov 29 17:02:43 CET 2012 <!-- hhmts end -->
+<!-- hhmts start -->Last modified: Thu Nov 29 20:13:55 CET 2012 <!-- hhmts end -->
 </small></div>
 <address>
 <a href="http://www.cse.chalmers.se/~hallgren/">TH</a>

src/www/minibar/minibar.css

@@ -82,3 +82,8 @@ span.brackets {
 div.brackets .token {
   padding: 0 0.5ex;
 }
+
+div.browse, table.browse td {
+    background: white;
+    padding: 2px;
+}

src/www/minibar/minibar.js

@@ -142,17 +142,48 @@ Minibar.prototype.change_grammar=function(grammar_info) {
 }
 
 Minibar.prototype.show_grammarinfo=function() {
-    this.translations.main.innerHTML=""
+    var t=this
     var g=this.grammar;
+    function draw_cats(cats) {
+	function draw_cat(cat) {
+	    var i=cats[cat]
+	    return tr([td(text(i.def)),
+		       td(text(i.producers.join(", "))),
+		       td(text(i.consumers.join(", ")))])
+	}
+	var table=wrap_class("table","browse",g.categories.map(draw_cat))
+	var hdr=tr([th(text("Category")),
+		    th(text("Producers")),
+		    th(text("Consumers"))])
+	insertFirst(table,hdr)
+	return table
+    }
+    function draw_funs(funs) {
+	function draw_fun(fun) {
+	    var def=funs[fun].def.split(":")
+	    return tr([td(text(def[0])),td(text(":")),td(text(def[1]||""))])
+	}
+	return div_class("browse",wrap("table",g.functions.map(draw_fun)))
+    }
+    function draw_more(info) {
+	replaceChildren(cats,draw_cats(info.cats))
+	replaceChildren(funs,draw_funs(info.funs))
+	btn.disabled=true;
+    }
+
+    function more() { t.server.browse({},draw_more) }
+
+    var cats=wrap("div",text(g.categories.join(", ")))
+    var funs=wrap("div",text(g.functions.join(", ")))
+    var btn=button("More info",more)
+
+    clear(t.translations.main)
     appendChildren(this.translations.main,
 		   [wrap("h3",text(g.name)),
-		    node("dl",{},
+		    btn,
-			 [dt(text("Start category")),
+		    wrap("h4",text("Start category")), text(g.startcat || ""),
-			  dd(text(g.startcat || "")),
+		    wrap("h4",text("Categories")), cats,
-			  dt(text("Categories")),
+		    wrap("h4",text("Functions")), funs])
-			  dd(text(g.categories.join(", "))),
-			  dt(text("Functions")),
-			  dd(text(g.functions.join(", ")))])])
 }
 
 Minibar.prototype.append_extra_buttons=function(extra,options) {