minibar: support for adding grammars from several servers to the grammar menu

You can also add grammars from several directories on the same server of course.
The included minibar configuration file adds the user's own grammars from the
grammar editor.

4 files changed, 53 insertions, 33 deletions

diff --git a/src/www/minibar/minibar.js b/src/www/minibar/minibar.js
index 86be6af7e..83a336434 100644
--- a/src/www/minibar/minibar.js
+++ b/src/www/minibar/minibar.js
@@ -53,6 +53,8 @@ function Minibar(server,opts) {
     with(this) {
 	appendChildren(menubar,[input.menus,translations.menus,input.buttons])
 	appendChildren(minibar,[menubar,input.main,translations.main,extra]);
+	if(options.help_url)
+	    menubar.appendChild(button("Help",bind(open_help,this)));
 	append_extra_buttons(extra,options);
     }
 
@@ -63,51 +65,63 @@ function Minibar(server,opts) {
 
     /* --- Main program, this gets things going ----------------------------- */
     with(this) {
-	if(server.grammar_list) show_grammarlist(server.grammar_list);
-	else server.get_grammarlist(bind(show_grammarlist,this));
+	server.get_grammarlists(bind(show_grammarlist,this));
     }
 }
 
-Minibar.prototype.show_grammarlist=function(grammars) {
+Minibar.prototype.show_grammarlist=function(dir,grammar_names,dir_count) {
     var t=this;
-    t.grammar_menu=empty_id("select","grammar_menu");
+    var first_time= !t.grammar_menu
+    if(first_time) {
+	t.grammar_menu=empty_id("select","grammar_menu");
+	t.grammars=[];
+	t.grammar_dirs=[];
+    }
     with(t) {
-	if(grammars.length>1) {
-	    function opt(g) { return option(g,g); }
-	    appendChildren(grammar_menu,map(opt,grammars));
-	    function pick() {
-		var grammar_name=grammar_menu.value
-		if(window.localStorage)
-		    localStorage["gf.minibar.last_grammar"]=grammar_name;
-		t.select_grammar(grammar_name);
-	    }
-    	    grammar_menu.onchange=bind(pick,this);
-	    insertFirst(menubar,button("i",bind(show_grammarinfo,this)))
-	    insertFirst(menubar,grammar_menu);
-	    insertFirst(menubar,text("Grammar: "));
+	grammar_dirs.push(dir);
+	grammars=grammars.concat(grammar_names.map(function(g){return dir+g}))
+	function glabel(g) {
+	    return hasPrefix(dir,"/tmp/gfse.") ? "gfse: "+g : g
 	}
-	if(options.help_url)
-	    menubar.appendChild(button("Help",bind(open_help,this)));
-	var grammar0=options.initial_grammar
-	if(!grammar0 && window.localStorage) {
-	    var last_grammar=localStorage["gf.minibar.last_grammar"];
-	    if(last_grammar)
-		for(var i in grammars)
-		    if(last_grammar==grammars[i]) grammar0=last_grammar;
+	function opt(g) { return option(glabel(g),dir+g); }
+	appendChildren(grammar_menu,map(opt,grammar_names));
+	function pick() {
+	    var grammar_url=grammar_menu.value
+	    if(window.localStorage)
+		localStorage["gf.minibar.last_grammar"]=grammar_url;
+	    t.select_grammar(grammar_url);
+	}
+	function pick_first_grammar() {
+	    if(t.timeout) clearTimeout(t.timeout),t.timeout=null;
+	    if(t.grammar_menu.length>1 && !t.grammar_menu.parentElement) {
+    		t.grammar_menu.onchange=bind(pick,t);
+		insertFirst(t.menubar,button("i",bind(t.show_grammarinfo,t)))
+		insertFirst(t.menubar,t.grammar_menu);
+		insertFirst(t.menubar,text("Grammar: "));
+	    }
+	    var grammar0=t.options.initial_grammar
+	    if(!grammar0 && window.localStorage) {
+		var last_grammar=localStorage["gf.minibar.last_grammar"];
+		if(last_grammar && elem(last_grammar,t.grammars))
+		    grammar0=last_grammar;
+	    }
+	    if(!grammar0) grammar0=t.grammars[0];
+	    t.grammar_menu.value=grammar0;
+	    t.select_grammar(grammar0);
 	}
-	if(!grammar0) grammar0=grammars[0];
-	grammar_menu.value=grammar0;
-	select_grammar(grammar0);
+	// Wait at most 1.5s before showing the grammar menu.
+	if(first_time) t.timeout=setTimeout(pick_first_grammar,1500);
+	if(t.grammar_dirs.length>=dir_count) pick_first_grammar();
     }
 }
 
-Minibar.prototype.select_grammar=function(grammar_name) {
+Minibar.prototype.select_grammar=function(grammar_url) {
     var t=this;
     //debug("select_grammar ");
     function change_grammar() {
 	t.server.grammar_info(bind(t.change_grammar,t));
     }
-    t.server.switch_grammar(grammar_name,change_grammar);
+    t.server.switch_to_other_grammar(grammar_url,change_grammar);
 }
 
 Minibar.prototype.change_grammar=function(grammar_info) {
diff --git a/src/www/minibar/minibar_input.js b/src/www/minibar/minibar_input.js
index ac354f83b..eb4b959be 100644
--- a/src/www/minibar/minibar_input.js
+++ b/src/www/minibar/minibar_input.js
@@ -415,7 +415,7 @@ Input.prototype.browse=function(id,cont) {
 	    t.grammar.browse[id]=info;
 	    cont(info);
 	}
-	server.browse(id,browsed);
+	t.server.browse(id,browsed);
     }
 }
 
diff --git a/src/www/minibar/minibar_online.js b/src/www/minibar/minibar_online.js
index fb7e2fc48..faeae9a7e 100644
--- a/src/www/minibar/minibar_online.js
+++ b/src/www/minibar/minibar_online.js
@@ -24,6 +24,11 @@ if(/^\?\/tmp\//.test(location.search)) {
     if(args[0]) online_options.grammars_url=args[0];
     if(args[1]) minibar_options.initial_grammar=args[1];
 }
+else if(window.localStorage) {
+    var s=localStorage["gf.editor.simple.grammardir"]
+    if(s) var editor_dir=JSON.parse(s);
+}
 
 var server=pgf_online(online_options);
+if(editor_dir) server.add_grammars_url(editor_dir+"/");
 var minibar=new Minibar(server,minibar_options);
diff --git a/src/www/minibar/pgf_online.js b/src/www/minibar/pgf_online.js
index b6329daba..970aae062 100644
--- a/src/www/minibar/pgf_online.js
+++ b/src/www/minibar/pgf_online.js
@@ -27,12 +27,13 @@ function pgf_online(options) {
 	    else http_get_json(this.grammars_url+"grammars.cgi",cont,err);
 	},
 	get_grammarlists: function(cont,err) { // May call cont several times!
+	    var ds=this.other_grammars_urls;
+	    var n=1+ds.length;
 	    function pair(dir) {
-		return function(grammar_list){cont(dir,grammar_list)}
+		return function(grammar_list){cont(dir,grammar_list,n)}
 	    }
 	    function ignore_error(err) { console.log(err) }
 	    this.get_grammarlist(pair(this.grammars_url),err)
-	    var ds=this.other_grammars_urls;
 	    for(var i in ds)
 		http_get_json(ds[i]+"grammars.cgi",pair(ds[i]),ignore_error);
 	},