Syntax editor: return to editor after having switched to minibar

1 files changed, 30 insertions, 13 deletions

diff --git a/src/www/syntax-editor/editor_online.js b/src/www/syntax-editor/editor_online.js
index feeb09efb..9edcf2947 100644
--- a/src/www/syntax-editor/editor_online.js
+++ b/src/www/syntax-editor/editor_online.js
@@ -20,21 +20,38 @@ var editor_options = {
 }
 if(window.Minibar) // Minibar loaded?
     editor_options.lin_action=function(s,langFrom) {
-        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: {
+        var editor=this;
+        var minibar_options = {
+            target: "minibar",
+            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,
                 input: s.split(" ") // is it that easy?
-	    }
-	}
-	editor.minibar=new Minibar(server,minibar_options);
+            },
+            // get us back to the editor!
+            abstract_action: function(tree) {
+                var minibar=this;
+                // how to get hold of new minibar?
+                var editor_options = {
+                    target: "editor",
+                    initial: {
+                        grammar: editor.minibar.grammar_menu.value, // hmm
+                        startcat: editor.minibar.input.startcat_menu.value, // hmm
+                        abstr: tree
+                    }
+                }
+                minibar.hide();
+                minibar.editor.show();
+            }
+        }
+        editor.hide();
+        editor.minibar=new Minibar(server,minibar_options);
+        editor.minibar.editor = editor; // :S
     }
 if(/^\?\/tmp\//.test(location.search)) {
     var args=decodeURIComponent(location.search.substr(1)).split(" ")