Simple Translation Tool: initial support for editing source segments in the minibar

src/www/minibar/minibar.html

@@ -27,12 +27,13 @@
 &amp; <a href="http://www.grammaticalframework.org:41296/translate/">Translator</a>]
 </small>
 <small class=modtime>
-HTML <!-- hhmts start -->Last modified: Fri Nov 23 16:07:35 CET 2012 <!-- hhmts end -->
+HTML <!-- hhmts start -->Last modified: Wed Apr  3 18:48:06 CEST 2013 <!-- hhmts end -->
 </small>
 <address>
 
 <script type="text/JavaScript" src="../js/grammar_manager.js"></script>
 <script type="text/JavaScript" src="../js/support.js"></script>
+<script type="text/JavaScript" src="../js/localstorage.js"></script>
 <script type="text/JavaScript" src="minibar.js"></script>
 <script type="text/JavaScript" src="minibar_input.js"></script>
 <script type="text/JavaScript" src="minibar_translations.js"></script>

src/www/minibar/minibar_input.js

@@ -40,7 +40,7 @@ function Input(server,translations,opts) { // Input object constructor
 
 	var o=options;
 	if(o.initial_grammar && o.initial && o.initial.from && o.initial.input)
-	    t.set_input_for(o.initial_grammar,o.initial.from,o.initial.input)
+	    t.set_input_for(o.initial_grammar,o.initial)
     }
 
     /* --- Input client state initialization --- */
@@ -89,11 +89,12 @@ Input.prototype.change_language=function () {
     this.add_words(new_input)
 }
 
-Input.prototype.set_input_for=function(grammar_url,from,new_input) {
+Input.prototype.set_input_for=function(grammar_url,initial) {
     var t=this
     var local=mi_local(grammar_url)
-    local.put("from",from)
-    local.put("current",{from:from,input:new_input})
+    local.put("from",initial.from)
+    local.put("current",{from:initial.from,input:initial.input})
+    if(initial.startcat) local.put("startcat",initial.startcat)
 }
 
 Input.prototype.clear_all2=function() {
@@ -484,26 +485,7 @@ Input.prototype.browse=function(id,cont) {
 
 
 function mi_local(grammar_url) {
-    function dummy() {
-	return {
-	    get: function(name,def) { return def },
-	    put: function(name,value) { }
-	}
-    }
-    function real() {
-	var prefix="gf.minibar_input."+grammar_url+"."
-	return {
-	    get: function (name,def) {
-		var id=prefix+name
-		return localStorage[id] ? JSON.parse(localStorage[id]) : def;
-	    },
-	    put: function (name,value) {
-		var id=prefix+name;
-		localStorage[id]=JSON.stringify(value);
-	    }
-	}
-    }
-    return window.localStorage ? real() : dummy()
+    return appLocalStorage("gf.minibar_input."+grammar_url+".")
 }
 
 

src/www/minibar/minibar_translations.js

@@ -28,6 +28,11 @@ function Translations(server,opts) {
     var tom=this.to_menu=node("select",{id:"to_menu",multiple:"",size:5},[]);
     appendChildren(this.menus,[text(" To: "), this.to_menu])
     tom.onchange=bind(this.change_language,this);
+    var o=this.options
+    if(o.initial_grammar && o.initial_toLangs) {
+	var local=mt_local(o.initial_grammar);
+	local.put("toLangs",o.initial_toLangs)
+    }
     /* // This seems triggers weird scrolling behavior in Firefox and Chrome:
     tom.onmouseover=function() { var n=tom.options.length;
 				 tom.size=n<12 ? n : 12; }
@@ -39,8 +44,9 @@ function Translations(server,opts) {
 Translations.prototype.change_grammar=function(grammar) {
     var t=this
     t.grammar=grammar;
-    
+
     t.local=mt_local(t.server.current_grammar_url)
+
     update_language_menu(t.to_menu,grammar);
     insertFirst(t.to_menu,option("All","All"));
     t.to_menu.value="All";
@@ -263,6 +269,10 @@ Translations.prototype.parsetree_button=function(abs,lang) {
 
 /* --- Auxiliary functions -------------------------------------------------- */
 
+function mt_local(grammar_url) {
+    return appLocalStorage("gf.minibar_translations."+grammar_url+".")
+}
+
 function tree_button(img_url,opt) {
     var imgs=[tree_icon,img_url+(opt||"&nofun=true"),img_url]
     var current=0;
@@ -283,31 +293,6 @@ function draw_brackets(b) {
 	       b.children.map(draw_brackets))
 }
 
-
-// Access to localStorage, if available
-function mt_local(grammar_url) {
-    function dummy() {
-	return {
-	    get: function(name,def) { return def },
-	    put: function(name,value) { }
-	}
-    }
-    function real() {
-	var prefix="gf.minibar_translations."+grammar_url+"."
-	return {
-	    get: function (name,def) {
-		var id=prefix+name
-		return localStorage[id] ? JSON.parse(localStorage[id]) : def;
-	    },
-	    put: function (name,value) {
-		var id=prefix+name;
-		localStorage[id]=JSON.stringify(value);
-	    }
-	}
-    }
-    return window.localStorage ? real() : dummy()
-}
-
 // Convert an array of strings to a set (for quick & easy membership tests)
 function toSet(a) {
     var set={}