diff --git a/src/runtime/javascript/minibar/minibar.js b/src/runtime/javascript/minibar/minibar.js index 39d741bbd..33b5de1be 100644 --- a/src/runtime/javascript/minibar/minibar.js +++ b/src/runtime/javascript/minibar/minibar.js @@ -1,21 +1,69 @@ +// minibar.js, assumes that support.js has also been loaded + +/* --- Configuration -------------------------------------------------------- */ var server="http://www.grammaticalframework.org:41296" //var server="http://tournesol.cs.chalmers.se:41296"; //var server="http://localhost:41296"; var grammars_url=server+"/grammars/"; -var current_grammar_url=grammars_url+"Foods.pgf"; var tree_icon=server+"/translate/se.chalmers.cs.gf.gwt.TranslateApp/tree-btn.png"; -function start_minibar() { +/* --- Grammar access object ------------------------------------------------ */ + +var server = { + // State variables (private): + current_grammar_url: grammars_url+"Foods.pgf", + // Methods: + switch_grammar: function(grammar_name) { + this.current_grammar_url=grammars_url+grammar_name; + }, + + get_grammarlist: function() { + jsonp(grammars_url+"grammars.cgi") // calls show_grammarlist + }, + get_languages: function(cont_name) { + jsonp(this.current_grammar_url,cont_name); + }, + get_random: function(cont_name) { + jsonp(this.current_grammar_url+"?command=random&random="+Math.random(),cont_name); + }, + linearize: function(tree,to,cont_name) { + jsonp(this.current_grammar_url+"?command=linearize&tree=" + +encodeURIComponent(tree)+"&to="+to,cont_name) + }, + complete: function(from,input,cont_name) { + jsonp(this.current_grammar_url + +"?command=complete" + +"&from="+encodeURIComponent(from) + +"&input="+encodeURIComponent(input), + cont_name); + + }, + translate: function(from,input,cont_name) { + jsonp(this.current_grammar_url + +"?command=translate" + +"&from="+encodeURIComponent(from) + +"&input="+encodeURIComponent(input), + cont_name) + } + +}; + +/* --- Initialisation ------------------------------------------------------- */ + +function start_minibar() { // typically called when the HTML document is loaded var minibar=element("minibar"); minibar.appendChild(div_id("menubar")); minibar.appendChild(div_id("surface")); minibar.appendChild(div_id("words")); minibar.appendChild(div_id("translations")); - jsonp(grammars_url+"grammars.cgi",""); // calls show_grammarlist + server.get_grammarlist(); // calls show_grammarlist } + +/* --- Functions ------------------------------------------------------------ */ + function show_grammarlist(grammars) { var menu=empty("select"); for(var i=0;i