helm/on-line/javascript/prelude.js

   1
   2 function getInitialProcessorURL()
   3 {
   4   var search = top.location.search;
   5   search = search.slice(1);
   6   var args = search.split("&");
   7   var processorURL = "-1";
   8   for (var i = 0 ; i < args.length ; i++) {
   9      var couple = args[i].split("=");
  10      if (couple[0] == "processorURL") processorURL = couple[1];
  11   }
  12   if (processorURL == "-1") processorURL = getDefaultParam("processorURL");
  13   return processorURL;
  14 }
  15
  16 function getInitialGetterURL()
  17 {
  18   var search = top.location.search;
  19   search = search.slice(1);
  20   var args = search.split("&");
  21   var getterURL = "-1";
  22   for (var i = 0 ; i < args.length ; i++) {
  23      var couple = args[i].split("=");
  24      if (couple[0] == "getterURL") getterURL = couple[1];
  25   }
  26   if (getterURL == "-1") getterURL = getDefaultParam("getterURL");
  27   return getterURL;
  28 }
  29
  30 function getInitialUNICODEvsSYMBOL()
  31 {
  32   var search = top.location.search;
  33   search = search.slice(1);
  34   var args = search.split("&");
  35   var UNICODEvsSYMBOL = "-1";
  36   for (var i = 0 ; i < args.length ; i++) {
  37      var couple = args[i].split("=");
  38      if (couple[0] == "UNICODEvsSYMBOL") UNICODEvsSYMBOL = couple[1];
  39   }
  40   if (UNICODEvsSYMBOL == "-1") UNICODEvsSYMBOL = getDefaultParam("UNICODEvsSYMBOL");
  41   return UNICODEvsSYMBOL;
  42 }
  43
  44 function getInitialUNICODEvsSYMBOLsymbol()
  45 {
  46   if (getInitialUNICODEvsSYMBOL() == "symbol")
  47    return "CHECKED";
  48   else
  49    return "";
  50 }
  51
  52 function getInitialUNICODEvsSYMBOLunicode()
  53 {
  54   if (getInitialUNICODEvsSYMBOL() == "unicode")
  55    return "CHECKED";
  56   else
  57    return "";
  58 }
  59
  60 function getUwoboURL()
  61 {
  62   return document.uwoboURL.elements[0].value;
  63 }
  64
  65 function getGetterURL()
  66 {
  67   return document.getterURL.elements[0].value;
  68 }
  69
  70 function getUNICODEvsSYMBOL()
  71 {
  72   if (document.UNICODEvsSYMBOL.radioUNICODEvsSYMBOL[0].checked)
  73    return document.UNICODEvsSYMBOL.radioUNICODEvsSYMBOL[0].value;
  74   else
  75    return document.UNICODEvsSYMBOL.radioUNICODEvsSYMBOL[1].value;
  76 }
  77
  78 function chopSlash(url)
  79 {
  80   return url.slice(0,url.lastIndexOf('/'));
  81 }
  82
  83 function refreshLinks()
  84 {
  85   var search = top.location.search;
  86   search = search.slice(1);
  87   var args = search.split("&");
  88   var cicuri = "-1", theoryuri = "-1", mode = "-1";
  89   for (var i = 0 ; i < args.length ; i++) {
  90      var couple = args[i].split("=");
  91      switch (couple[0]) {
  92         case "cicuri"       : cicuri     =couple[1]; break;
  93         case "theoryuri"    : theoryuri  =couple[1]; break;
  94         case "mode"         : mode       =couple[1]; break;
  95      }
  96   }
  97   if (cicuri == "-1") cicuri = getDefaultParam("cicuri");
  98   if (theoryuri == "-1") theoryuri = getDefaultParam("theoryuri");
  99   if (mode == "-1") mode = getDefaultParam("mode");
 100
 101   document.links[2].search = "?getterURL=" + getGetterURL();
 102
 103   document.links[3].search =
 104     "?processorURL=" + getUwoboURL() +
 105     "&getterURL=" + getGetterURL();
 106
 107   var topurl =
 108    chopSlash(chopSlash(
 109     document.location.protocol + '//' +
 110     document.location.host +
 111     document.location.pathname));
 112   document.links[4].href =
 113      getUwoboURL() + "apply" +
 114       "?keys=RT" +
 115       "&param.topurl=" + topurl +
 116       "&xmluri=" +
 117       escape(
 118        topurl + "/html/library/index.html" +
 119        "?cicuri=" + cicuri +
 120        "&theoryuri=" + theoryuri +
 121        "&mode=" + mode +
 122        "&processorURL=" + getUwoboURL() +
 123        "&getterURL=" + getGetterURL() +
 124        "&UNICODEvsSYMBOL=" + getUNICODEvsSYMBOL()
 125       );
 126 }
 127
 128 function selectUwoboURL(ss)
 129 {
 130   if (ss.selectedIndex == 0) {
 131     document.uwoboURL.elements[0].value = "";
 132   } else {
 133     document.uwoboURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":8080/helm/servlet/uwobo/";
 134   }
 135
 136   refreshLinks();
 137 }
 138
 139 function selectGetterURL(ss)
 140 {
 141   if (ss.selectedIndex == 0) {
 142     document.getterURL.elements[0].value = "";
 143   } else {
 144     document.getterURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":8081/";
 145   }
 146
 147   refreshLinks();
 148 }