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