minibar: default input language is now the user's preferred language, if possible

This is implemented using the userLanguage field in the grammar info output by
pgf-server.

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);