From d63724ed5022d58620a9738ae359cd3e39446a2f Mon Sep 17 00:00:00 2001
From: hallgren <hallgren@chalmers.se>
Date: Tue, 18 Oct 2011 14:34:00 +0000
Subject: [PATCH] minibar: add a button to show some grammar info

---
 src/www/minibar/minibar.js | 15 +++++++++++++++
 src/www/minibar/support.js |  1 +
 2 files changed, 16 insertions(+)

diff --git a/src/www/minibar/minibar.js b/src/www/minibar/minibar.js
index 778a3957b..a94cc5629 100644
--- a/src/www/minibar/minibar.js
+++ b/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)
diff --git a/src/www/minibar/support.js b/src/www/minibar/support.js
index c65c1a389..962426d53 100644
--- a/src/www/minibar/support.js
+++ b/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); }