Some work on minibar:

1. Menu for choosing target language.
2. Pass options when calling start_minibar.
See about.html for more details.

src/runtime/javascript/minibar/support.js

@@ -74,6 +74,12 @@ function button(label,action) {
   return el;
 }
 
+function option(label,value) {
+    var el=empty("option","value",value);
+    el.innerHTML=label;
+    return el;
+}
+
 function appendChildren(el,cs) {
   for(var i=0;i<cs.length;i++)
     el.appendChild(cs[i]);