minibar: can now switch back to the minibar after switching to the syntax editor

This is done by including a lin_action when starting the syntax editor from
the minibar.
Also: added some minibar options in the syntax editor for consistency...

src/www/minibar/minibar_input.js

@@ -39,11 +39,8 @@ function Input(server,translations,opts) { // Input object constructor
 	    buttons.appendChild(button("Random",bind(generate_random,t),"R"));
 
 	var o=options;
-	if(o.initial_grammar && o.initial && o.initial.from && o.initial.input){
+	if(o.initial_grammar && o.initial && o.initial.from && o.initial.input)
-	    t.local=mi_local(o.initial_grammar)
+	    t.set_input_for(o.initial_grammar,o.initial.from,o.initial.input)
-	    t.local.put("from",o.initial.from)
-	    t.local.put("current",o.initial)
-	}
     }
 
     /* --- Input client state initialization --- */
@@ -92,6 +89,13 @@ Input.prototype.change_language=function () {
     this.add_words(new_input)
 }
 
+Input.prototype.set_input_for=function(grammar_url,from,new_input) {
+    var t=this
+    var local=mi_local(grammar_url)
+    local.put("from",from)
+    local.put("current",{from:from,input:new_input})
+}
+
 Input.prototype.clear_all2=function() {
     with(this) {
 	current.input=[];

src/www/minibar/minibar_online.js

@@ -27,10 +27,29 @@ if(window.Editor) // Syntax editor loaded?
 	    initial: { grammar: minibar.grammar_menu.value, // hmm
 		       startcat: minibar.input.startcat_menu.value, // hmm
 		       abstr: tree
-		     }
+		     },
+	    lin_action: function(new_input,langFrom) {
+		var grammar_url=editor.menu.ui.grammar_menu.value // hmm
+		minibar.input.set_input_for(grammar_url,langFrom,
+					    gf_lex(new_input))
+
+		//Easier: delete the editor and create a new one next time:
+		clear(editor.container)
+		editor=null;
+
+		//Better: keep editor around and reactivate it next time:
+		//editor.container.style.display="none"
+
+		// Even if the grammar is the same as before, this call is
+		// what eventually triggers the new_input to be loaded:
+		minibar.select_grammar(grammar_url)
+
+		// Make the minibar visible again
+		minibar.minibar.style.display=""
+	    }
 	}
-	minibar.minibar.style.display="none"
+	minibar.minibar.style.display="none" // Hide the minibar
-	minibar.editor=new Editor(server,editor_options)
+	var editor=new Editor(server,editor_options)
     }
 
 if(/^\?\/tmp\//.test(location.search)) {

src/www/syntax-editor/editor_online.js

@@ -23,6 +23,11 @@ if(window.Minibar) // Minibar loaded?
         editor.shutdown();
 	var minibar_options = {
 	    target: "editor",
+	    show_abstract: true,
+	    show_trees: true,
+	    show_grouped_translations: false,
+	    show_brackets: true,
+	    word_replacements: true,
 	    initial_grammar: editor.menu.ui.grammar_menu.value, // hmm
 	    initial: {
                 from: langFrom,