From 846b747cee6f543bc17745bb75a2dadce2d5d803 Mon Sep 17 00:00:00 2001
From: hallgren <hallgren@chalmers.se>
Date: Fri, 10 Sep 2010 11:03:46 +0000
Subject: [PATCH] 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.
---
 src/runtime/javascript/minibar/minibar.js | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

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