diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/www/minibar/minibar.js | 74 | ||||
| -rw-r--r-- | src/www/minibar/minibar_input.js | 2 | ||||
| -rw-r--r-- | src/www/minibar/minibar_online.js | 5 | ||||
| -rw-r--r-- | src/www/minibar/pgf_online.js | 5 |
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); }, |