diff options
| author | hallgren <hallgren@chalmers.se> | 2012-11-22 16:42:39 +0000 |
|---|---|---|
| committer | hallgren <hallgren@chalmers.se> | 2012-11-22 16:42:39 +0000 |
| commit | 24bf1f0d0ea42286a40cc8ac734b7d99c4197736 (patch) | |
| tree | 6548f69df2f50195e117b07f552bea4ebfb9dd34 /src/www/minibar/minibar_online.js | |
| parent | db544b1cc9ee72c87dd6bbd094f6985b9e436186 (diff) | |
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...
Diffstat (limited to 'src/www/minibar/minibar_online.js')
| -rw-r--r-- | src/www/minibar/minibar_online.js | 25 |
1 files changed, 22 insertions, 3 deletions
diff --git a/src/www/minibar/minibar_online.js b/src/www/minibar/minibar_online.js index bf3f3f6de..c4bc61039 100644 --- a/src/www/minibar/minibar_online.js +++ b/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.editor=new Editor(server,editor_options) + minibar.minibar.style.display="none" // Hide the minibar + var editor=new Editor(server,editor_options) } if(/^\?\/tmp\//.test(location.search)) { |