UNICODEvsSYMBOL parameter now added everywhere

[helm.git] / helm / on-line / javascript / prelude.js

diff --git a/helm/on-line/javascript/prelude.js b/helm/on-line/javascript/prelude.js
index 90e877a01381e934b5caa2e6adfbd5b82afc7fc0..12862e545024b4b116acc010a9f5555063c6667c 100644 (file)
--- a/helm/on-line/javascript/prelude.js
+++ b/helm/on-line/javascript/prelude.js
@@ -27,6 +27,36 @@ function getInitialGetterURL()
   return getterURL;
 }
 
+function getInitialUNICODEvsSYMBOL()
+{
+  var search = top.location.search;
+  search = search.slice(1);
+  var args = search.split("&");
+  var UNICODEvsSYMBOL = "-1";
+  for (var i = 0 ; i < args.length ; i++) {
+     var couple = args[i].split("=");
+     if (couple[0] == "UNICODEvsSYMBOL") UNICODEvsSYMBOL = couple[1];
+  }
+  if (UNICODEvsSYMBOL == "-1") UNICODEvsSYMBOL = getDefaultParam("UNICODEvsSYMBOL");
+  return UNICODEvsSYMBOL;
+}
+
+function getInitialUNICODEvsSYMBOLsymbol()
+{
+  if (getInitialUNICODEvsSYMBOL() == "symbol")
+   return "CHECKED";
+  else
+   return "";
+}
+
+function getInitialUNICODEvsSYMBOLunicode()
+{
+  if (getInitialUNICODEvsSYMBOL() == "unicode")
+   return "CHECKED";
+  else
+   return "";
+}
+
 function getUwoboURL()
 {
   return document.uwoboURL.elements[0].value;
@@ -37,6 +67,14 @@ function getGetterURL()
   return document.getterURL.elements[0].value;
 }
 
+function getUNICODEvsSYMBOL()
+{
+  if (document.UNICODEvsSYMBOL.radioUNICODEvsSYMBOL[0].checked)
+   return document.UNICODEvsSYMBOL.radioUNICODEvsSYMBOL[0].value;
+  else
+   return document.UNICODEvsSYMBOL.radioUNICODEvsSYMBOL[1].value;
+}
+
 function refreshLinks()
 {
   var search = top.location.search;
@@ -65,7 +103,8 @@ function refreshLinks()
      + "&theoryuri=" + theoryuri
      + "&mode=" + mode
      + "&processorURL=" + getUwoboURL()
-     + "&getterURL=" + getGetterURL();
+     + "&getterURL=" + getGetterURL()
+     + "&UNICODEvsSYMBOL=" + getUNICODEvsSYMBOL();
 }
 
 function selectUwoboURL(ss)
@@ -76,7 +115,7 @@ function selectUwoboURL(ss)
     document.uwoboURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":8080/helm/servlet/uwobo/";
   }
 
-  refreshLink();
+  refreshLinks();
 }
 
 function selectGetterURL(ss)
@@ -87,5 +126,5 @@ function selectGetterURL(ss)
     document.getterURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":8081/";
   }
 
-  refreshLink();
+  refreshLinks();
 }