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 getInitialDrawGraphURL()
  31 {
  32   var search = top.location.search;
  33   search = search.slice(1);
  34   var args = search.split("&");
  35   var draw_graphURL = "-1";
  36   for (var i = 0 ; i < args.length ; i++) {
  37      var couple = args[i].split("=");
  38      if (couple[0] == "draw_graphURL") draw_graphURL = couple[1];
  39   }
  40   if (draw_graphURL == "-1") draw_graphURL = getDefaultParam("draw_graphURL");
  41   return draw_graphURL;
  42 }
  43
  44 function getInitialURISetQueueURL()
  45 {
  46   var search = top.location.search;
  47   search = search.slice(1);
  48   var args = search.split("&");
  49   var uri_set_queueURL = "-1";
  50   for (var i = 0 ; i < args.length ; i++) {
  51      var couple = args[i].split("=");
  52      if (couple[0] == "uri_set_queueURL") uri_set_queueURL = couple[1];
  53   }
  54   if (uri_set_queueURL == "-1") uri_set_queueURL = getDefaultParam("uri_set_queueURL");
  55   return uri_set_queueURL;
  56 }
  57
  58 function getInitialUNICODEvsSYMBOL()
  59 {
  60   var search = top.location.search;
  61   search = search.slice(1);
  62   var args = search.split("&");
  63   var UNICODEvsSYMBOL = "-1";
  64   for (var i = 0 ; i < args.length ; i++) {
  65      var couple = args[i].split("=");
  66      if (couple[0] == "UNICODEvsSYMBOL") UNICODEvsSYMBOL = couple[1];
  67   }
  68   if (UNICODEvsSYMBOL == "-1") UNICODEvsSYMBOL = getDefaultParam("UNICODEvsSYMBOL");
  69   return UNICODEvsSYMBOL;
  70 }
  71
  72 function getInitialUNICODEvsSYMBOLsymbol()
  73 {
  74   if (getInitialUNICODEvsSYMBOL() == "symbol")
  75    return "CHECKED";
  76   else
  77    return "";
  78 }
  79
  80 function getInitialUNICODEvsSYMBOLunicode()
  81 {
  82   if (getInitialUNICODEvsSYMBOL() == "unicode")
  83    return "CHECKED";
  84   else
  85    return "";
  86 }
  87
  88 function getUwoboURL()
  89 {
  90   return document.uwoboURL.elements[0].value;
  91 }
  92
  93 function getGetterURL()
  94 {
  95   return document.getterURL.elements[0].value;
  96 }
  97
  98 function getDrawGraphURL()
  99 {
 100   return document.draw_graphURL.elements[0].value;
 101 }
 102
 103 function getURISetQueueURL()
 104 {
 105   return document.uri_set_queueURL.elements[0].value;
 106 }
 107
 108 function getUNICODEvsSYMBOL()
 109 {
 110   if (document.UNICODEvsSYMBOL.radioUNICODEvsSYMBOL[0].checked)
 111    return document.UNICODEvsSYMBOL.radioUNICODEvsSYMBOL[0].value;
 112   else
 113    return document.UNICODEvsSYMBOL.radioUNICODEvsSYMBOL[1].value;
 114 }
 115
 116 function chopSlash(url)
 117 {
 118   return url.slice(0,url.lastIndexOf('/'));
 119 }
 120
 121 function refreshLinks()
 122 {
 123   var search = top.location.search;
 124   search = search.slice(1);
 125   var args = search.split("&");
 126   var cicuri = "-1", theoryuri = "-1", mode = "-1";
 127   for (var i = 0 ; i < args.length ; i++) {
 128      var couple = args[i].split("=");
 129      switch (couple[0]) {
 130         case "cicuri"       : cicuri     =couple[1]; break;
 131         case "theoryuri"    : theoryuri  =couple[1]; break;
 132         case "mode"         : mode       =couple[1]; break;
 133      }
 134   }
 135   if (cicuri == "-1") cicuri = getDefaultParam("cicuri");
 136   if (theoryuri == "-1") theoryuri = getDefaultParam("theoryuri");
 137   if (mode == "-1") mode = getDefaultParam("mode");
 138
 139   document.links[2].href =
 140    document.links[2].protocol + '//' +
 141    document.links[2].host +
 142    document.links[2].pathname +
 143    "?getterURL=" + getGetterURL();
 144
 145   document.links[3].href =
 146    document.links[3].protocol + '//' +
 147    document.links[3].host +
 148    document.links[3].pathname +
 149    "?processorURL=" + getUwoboURL() +
 150    "&getterURL=" + getGetterURL();
 151
 152   var topurl =
 153    chopSlash(chopSlash(
 154     document.location.protocol + '//' +
 155     document.location.host +
 156     document.location.pathname));
 157   document.links[4].href =
 158      getUwoboURL() + "apply" +
 159       "?keys=RT" +
 160       "&param.topurl=" + topurl +
 161       "&xmluri=" +
 162       escape(
 163        topurl + "/html/library/index.html" +
 164        "?cicuri=" + cicuri +
 165        "&theoryuri=" + theoryuri +
 166        "&mode=" + mode +
 167        "&processorURL=" + getUwoboURL() +
 168        "&getterURL=" + getGetterURL() +
 169        "&draw_graphURL=" + getDrawGraphURL() +
 170        "&uri_set_queueURL=" + getURISetQueueURL() +
 171        "&UNICODEvsSYMBOL=" + getUNICODEvsSYMBOL()
 172       );
 173 }
 174
 175 function selectUwoboURL(ss)
 176 {
 177   if (ss.selectedIndex == 0) {
 178     document.uwoboURL.elements[0].value = "";
 179   } else {
 180     document.uwoboURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":8080/helm/servlet/uwobo/";
 181   }
 182
 183   refreshLinks();
 184 }
 185
 186 function selectGetterURL(ss)
 187 {
 188   if (ss.selectedIndex == 0) {
 189     document.getterURL.elements[0].value = "";
 190   } else {
 191     document.getterURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":8081/";
 192   }
 193
 194   refreshLinks();
 195 }
 196
 197 function selectDrawGraphURL(ss)
 198 {
 199   if (ss.selectedIndex == 0) {
 200     document.draw_graphURL.elements[0].value = "";
 201   } else {
 202     document.draw_graphURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":8083/";
 203   }
 204
 205   refreshLinks();
 206 }
 207
 208 function selectURISetQueueURL(ss)
 209 {
 210   if (ss.selectedIndex == 0) {
 211     document.uri_set_queueURL.elements[0].value = "";
 212   } else {
 213     document.uri_set_queueURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":8084/";
 214   }
 215
 216   refreshLinks();
 217 }