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(defaultValue)
  88 {
  89   if (defaultValue == "symbol")
  90    return "CHECKED";
  91   else
  92    return "";
  93 }
  94
  95 function getInitialUNICODEvsSYMBOLunicode(defaultValue)
  96 {
  97   if (defaultValue == "unicode")
  98    return "CHECKED";
  99   else
 100    return "";
 101 }
 102
 103 function getProfileId()
 104 {
 105   return document.profile.elements[0].value;
 106 }
 107
 108 function getUwoboURL()
 109 {
 110   return document.uwoboURL.elements[0].value;
 111 }
 112
 113 function getGetterURL()
 114 {
 115   return document.getterURL.elements[0].value;
 116 }
 117
 118 function getProofCheckerURL()
 119 {
 120   return document.proofcheckerURL.elements[0].value;
 121 }
 122
 123 function getDrawGraphURL()
 124 {
 125   return document.draw_graphURL.elements[0].value;
 126 }
 127
 128 function getURISetQueueURL()
 129 {
 130   return document.uri_set_queueURL.elements[0].value;
 131 }
 132
 133 function getRdflyURL()
 134 {
 135   return document.rdflyURL.elements[0].value;
 136 }
 137
 138 function getUNICODEvsSYMBOL()
 139 {
 140   if (document.UNICODEvsSYMBOL.radioUNICODEvsSYMBOL[0].checked)
 141    return 'symbol';
 142   else
 143    return 'unicode';
 144 }
 145
 146 function getNaturalLanguage()
 147 {
 148   if (document.naturalLanguage.elements[0].checked)
 149    return 'yes';
 150   else
 151    return 'no';
 152 }
 153
 154 function getMaxGraphSize()
 155 {
 156   return document.maxGraphSize.elements[0].value;
 157 }
 158
 159 function getUpdateURL()
 160 {
 161   return '&param.processorURL=' + escape(getUwoboURL()) +
 162     '&param.getterURL=' + escape(getGetterURL()) +
 163     '&param.uri_set_queueURL=' + escape(getURISetQueueURL()) +
 164     '&param.draw_graphURL=' + escape(getDrawGraphURL()) +
 165     '&param.proofcheckerURL=' + escape(getProofCheckerURL()) +
 166     '&param.rdflyURL=' + escape(getRdflyURL()) +
 167     '&param.naturalLanguage=' + escape(getNaturalLanguage()) +
 168     '&param.uri_set_size=' + escape(getMaxGraphSize()) +
 169     '&param.UNICODEvsSYMBOL=' + escape(getUNICODEvsSYMBOL());
 170 }
 171
 172 function chopSlash(url)
 173 {
 174   return url.slice(0,url.lastIndexOf('/'));
 175 }
 176
 177 function refreshLinks()
 178 {
 179   var search = top.location.search;
 180   search = search.slice(1);
 181   var args = search.split("&");
 182   var cicuri = "-1", theoryuri = "-1", mode = "-1";
 183   for (var i = 0 ; i < args.length ; i++) {
 184      var couple = args[i].split("=");
 185      switch (couple[0]) {
 186         case "cicuri"       : cicuri     =couple[1]; break;
 187         case "theoryuri"    : theoryuri  =couple[1]; break;
 188         case "mode"         : mode       =couple[1]; break;
 189      }
 190   }
 191   if (cicuri == "-1") cicuri = getDefaultParam("cicuri");
 192   if (theoryuri == "-1") theoryuri = getDefaultParam("theoryuri");
 193   if (mode == "-1") mode = getDefaultParam("mode");
 194
 195   document.links[2].href =
 196    document.links[2].protocol + '//' +
 197    document.links[2].host +
 198    document.links[2].pathname +
 199    "?getterURL=" + getGetterURL();
 200
 201   document.links[3].href =
 202    document.links[3].protocol + '//' +
 203    document.links[3].host +
 204    document.links[3].pathname +
 205    "?processorURL=" + getUwoboURL() +
 206    "&getterURL=" + getGetterURL();
 207
 208   var topurl =
 209    chopSlash(chopSlash(
 210     document.location.protocol + '//' +
 211     document.location.host +
 212     document.location.pathname));
 213   document.links[4].href =
 214      getUwoboURL() + "apply" +
 215       "?keys=RT" +
 216       "&param.topurl=" + topurl +
 217       "&xmluri=" +
 218       escape(
 219        topurl + "/html/library/index.html" +
 220        "?cicuri=" + cicuri +
 221        "&theoryuri=" + theoryuri +
 222        "&mode=" + mode +
 223        "&processorURL=" + getUwoboURL() +
 224        "&getterURL=" + getGetterURL() +
 225        "&proofcheckerURL=" + getProofCheckerURL() +
 226        "&draw_graphURL=" + getDrawGraphURL() +
 227        "&uri_set_queueURL=" + getURISetQueueURL() +
 228        "&UNICODEvsSYMBOL=" + getUNICODEvsSYMBOL()
 229       );
 230 }
 231
 232 function selectUwoboURL(ss)
 233 {
 234   if (ss.selectedIndex == 0) {
 235     document.uwoboURL.elements[0].value = "";
 236   } else {
 237     document.uwoboURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":58080/";
 238   }
 239 }
 240
 241 function selectGetterURL(ss)
 242 {
 243   if (ss.selectedIndex == 0) {
 244     document.getterURL.elements[0].value = "";
 245   } else {
 246     document.getterURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":58081/";
 247   }
 248 }
 249
 250 function selectProofCheckerURL(ss)
 251 {
 252   if (ss.selectedIndex == 0) {
 253     document.proofcheckerURL.elements[0].value = "";
 254   } else {
 255     document.proofcheckerURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":58084/";
 256   }
 257 }
 258
 259 function selectDrawGraphURL(ss)
 260 {
 261   if (ss.selectedIndex == 0) {
 262     document.draw_graphURL.elements[0].value = "";
 263   } else {
 264     document.draw_graphURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":58083/";
 265   }
 266 }
 267
 268 function selectURISetQueueURL(ss)
 269 {
 270   if (ss.selectedIndex == 0) {
 271     document.uri_set_queueURL.elements[0].value = "";
 272   } else {
 273     document.uri_set_queueURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":58082/";
 274   }
 275 }
 276
 277 function selectRdflyURL(ss)
 278 {
 279   if (ss.selectedIndex == 0) {
 280     document.rdflyURL.elements[0].value = "";
 281   } else {
 282     document.rdflyURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":58086/";
 283   }
 284 }
 285
 286 function selectProfile(ss, interfaceURL)
 287 {
 288   location = getUwoboURL() +
 289     'apply?keys=SPK&param.processorURL=' + escape(getUwoboURL()) +
 290     '&param.profile=' + escape(ss.options[ss.selectedIndex].value) +
 291     '&xmluri=' + escape(interfaceURL + 'html/configuration.html');
 292 }
 293
 294 function saveProfile(origProfileId)
 295 {
 296   var profileId = getProfileId();
 297   var exists = false;
 298   var i;
 299   var options = document.profileList.elements[0];
 300   for (i = 0; i < options.length; i++)
 301     if (profileId == options[i].value) exists = true;
 302   if (exists) {
 303     if (confirm('Update the profile \'' + profileId + '\'?'))
 304       location = getUwoboURL() + 'setparams?id=' + profileId + getUpdateURL();
 305   } else {
 306     if (confirm('Create a new profile \'' + profileId + '\' with the current settings?'))
 307       location = getUwoboURL() + 'createprofile?id=' + profileId + '&orig=' + origProfileId + getUpdateURL();
 308   }
 309 }
 310