diff options
| author | hallgren <hallgren@chalmers.se> | 2010-06-02 13:59:38 +0000 |
|---|---|---|
| committer | hallgren <hallgren@chalmers.se> | 2010-06-02 13:59:38 +0000 |
| commit | e5bc4328cbeedd8f6235218e014e25b8060d20e8 (patch) | |
| tree | 37ac1af35fd186c8f3efd9f0dc979110388a22af | |
| parent | 86da023392276db274ffeb19184af2f336de6aac (diff) | |
New minibar option: default_source_language
| -rw-r--r-- | src/runtime/javascript/minibar/minibar.js | 9 | ||||
| -rw-r--r-- | 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"> |
