From 47285fe880001d368731ecc731021b472d2acbf1 Mon Sep 17 00:00:00 2001
From: hallgren <hallgren@chalmers.se>
Date: Wed, 2 Jun 2010 13:59:38 +0000
Subject: [PATCH] New minibar option: default_source_language

---
 src/runtime/javascript/minibar/minibar.js      | 9 ++++++++-
 src/runtime/javascript/minibar/phrasebook.html | 3 ++-
 2 files changed, 10 insertions(+), 2 deletions(-)

diff --git a/src/runtime/javascript/minibar/minibar.js b/src/runtime/javascript/minibar/minibar.js
index dcd65c6d5..8e7ab8172 100644
--- a/src/runtime/javascript/minibar/minibar.js
+++ b/src/runtime/javascript/minibar/minibar.js
@@ -15,6 +15,7 @@ var options={
     show_trees: false,
     show_grouped_translations: true,
     delete_button_text: "⌫",
+    default_source_language: null,
     try_google: true,
     feedback_url: null,
     help_url: null
@@ -142,7 +143,13 @@ 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) {
+	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);
+	    if(l==options.default_source_language) menu.selectedIndex=i;
+	}
+    }
     var to=element("to_menu");
     to.langmenu=menu;
     to.setAttribute("onchange","change_tolang(this)");
diff --git a/src/runtime/javascript/minibar/phrasebook.html b/src/runtime/javascript/minibar/phrasebook.html
index ec3ab12ec..73c0e849b 100644
--- a/src/runtime/javascript/minibar/phrasebook.html
+++ b/src/runtime/javascript/minibar/phrasebook.html
@@ -12,7 +12,8 @@ var phrasebook_options={
   grammar_list: ["Phrasebook.pgf"],
   delete_button_text: "Del",
   help_url: "http://www.grammaticalframework.org/examples/phrasebook/help-phrasebook.html",
-  feedback_url: "feedback.html"
+  feedback_url: "feedback.html",
+  default_source_language: "Eng"
 }
 </script>
 <meta name = "viewport" content = "width = device-width">