minibar: add a button to show some grammar info

src/www/minibar/minibar.js

@@ -75,6 +75,7 @@ Minibar.prototype.show_grammarlist=function(grammars) {
 	    appendChildren(grammar_menu,map(opt,grammars));
     	    grammar_menu.onchange=
 		bind(function() { select_grammar(grammar_menu.value); },this);
+	    insertFirst(menubar,button("i",bind(show_grammarinfo,this)))
 	    insertFirst(menubar,grammar_menu);
 	    insertFirst(menubar,text("Grammar: "));
 	}
@@ -104,6 +105,20 @@ Minibar.prototype.change_grammar=function(grammar_info) {
     }
 }
 
+Minibar.prototype.show_grammarinfo=function() {
+    this.translations.main.innerHTML=""
+    var g=this.grammar;
+    appendChildren(this.translations.main,
+		   [wrap("h3",text(g.name)),
+		    node("dl",{},
+			 [dt(text("Start category")),
+			  dd(text(g.startcat || "")),
+			  dt(text("Categories")),
+			  dd(text(g.categories.join(", "))),
+			  dt(text("Functions")),
+			  dd(text(g.functions.join(", ")))])])
+}
+
 Minibar.prototype.append_extra_buttons=function(extra,options) {
     with(this) {
 	if(options.try_google)

src/www/minibar/support.js

@@ -157,6 +157,7 @@ function div_class(cls,contents)  { return wrap_class("div",cls,contents); }
 
 function p(contents) { return wrap("p",contents); }
 function dt(contents) { return wrap("dt",contents); }
+function dd(contents) { return wrap("dd",contents); }
 function li(contents) { return wrap("li",contents); }
 
 function th(contents) { return wrap("th",contents); }