diff options
| -rw-r--r-- | src/runtime/javascript/minibar/minibar.js | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/src/runtime/javascript/minibar/minibar.js b/src/runtime/javascript/minibar/minibar.js index d586ffa5a..b85fc4726 100644 --- a/src/runtime/javascript/minibar/minibar.js +++ b/src/runtime/javascript/minibar/minibar.js @@ -140,7 +140,14 @@ function show_languages(grammar) { for(var i=0; i<lang.length; i++) if(/*lang[i].canParse &&*/ !hasPrefix(lang[i].name,"Disamb")) menu.appendChild(option(langpart(lang[i].name,grammar.name),""+i)); - if(options.default_source_language) { + if(grammar.userLanguage) { + for(var i=0;i<menu.options.length;i++) { + var ix=menu.options[i].value; + var l=menu.grammar.languages[ix].name; + if(l==grammar.userLanguage) menu.selectedIndex=i; + } + } + else if(options.default_source_language) { for(var i=0;i<menu.options.length;i++) { var ix=menu.options[i].value; var l=langpart(menu.grammar.languages[ix].name,menu.grammar.name); |