X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Fon-line%2Fjavascript%2Fprelude.js;fp=helm%2Fon-line%2Fjavascript%2Fprelude.js;h=0000000000000000000000000000000000000000;hp=83cff42bc5d2541db61bc284aaff3a50a0166093;hb=869549224eef6278a48c16ae27dd786376082b38;hpb=89262281b6e83bd2321150f81f1a0583645eb0c8

diff --git a/helm/on-line/javascript/prelude.js b/helm/on-line/javascript/prelude.js
deleted file mode 100644
index 83cff42bc..000000000
--- a/helm/on-line/javascript/prelude.js
+++ /dev/null
@@ -1,249 +0,0 @@
-
-function getInitialProcessorURL()
-{
-  var search = top.location.search;
-  search = search.slice(1);
-  var args = search.split("&");
-  var processorURL = "-1";
-  for (var i = 0 ; i < args.length ; i++) {
-     var couple = args[i].split("=");
-     if (couple[0] == "processorURL") processorURL = couple[1];
-  }
-  if (processorURL == "-1") processorURL = getDefaultParam("processorURL");
-  return processorURL;
-}
-
-function getInitialGetterURL()
-{
-  var search = top.location.search;
-  search = search.slice(1);
-  var args = search.split("&");
-  var getterURL = "-1";
-  for (var i = 0 ; i < args.length ; i++) {
-     var couple = args[i].split("=");
-     if (couple[0] == "getterURL") getterURL = couple[1];
-  }
-  if (getterURL == "-1") getterURL = getDefaultParam("getterURL");
-  return getterURL;
-}
-
-function getInitialProofCheckerURL()
-{
-  var search = top.location.search;
-  search = search.slice(1);
-  var args = search.split("&");
-  var proofcheckerURL = "-1";
-  for (var i = 0 ; i < args.length ; i++) {
-     var couple = args[i].split("=");
-     if (couple[0] == "proofcheckerURL") proofcheckerURL = couple[1];
-  }
-  if (proofcheckerURL == "-1")
-     proofcheckerURL = getDefaultParam("proofcheckerURL");
-  return proofcheckerURL;
-}
-
-function getInitialDrawGraphURL()
-{
-  var search = top.location.search;
-  search = search.slice(1);
-  var args = search.split("&");
-  var draw_graphURL = "-1";
-  for (var i = 0 ; i < args.length ; i++) {
-     var couple = args[i].split("=");
-     if (couple[0] == "draw_graphURL") draw_graphURL = couple[1];
-  }
-  if (draw_graphURL == "-1") draw_graphURL = getDefaultParam("draw_graphURL");
-  return draw_graphURL;
-}
-
-function getInitialURISetQueueURL()
-{
-  var search = top.location.search;
-  search = search.slice(1);
-  var args = search.split("&");
-  var uri_set_queueURL = "-1";
-  for (var i = 0 ; i < args.length ; i++) {
-     var couple = args[i].split("=");
-     if (couple[0] == "uri_set_queueURL") uri_set_queueURL = couple[1];
-  }
-  if (uri_set_queueURL == "-1") uri_set_queueURL = getDefaultParam("uri_set_queueURL");
-  return uri_set_queueURL;
-}
-
-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;
-}
-
-function getGetterURL()
-{
-  return document.getterURL.elements[0].value;
-}
-
-function getProofCheckerURL()
-{
-  return document.proofcheckerURL.elements[0].value;
-}
-
-function getDrawGraphURL()
-{
-  return document.draw_graphURL.elements[0].value;
-}
-
-function getURISetQueueURL()
-{
-  return document.uri_set_queueURL.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 chopSlash(url)
-{
-  return url.slice(0,url.lastIndexOf('/'));
-}
-
-function refreshLinks()
-{
-  var search = top.location.search;
-  search = search.slice(1);
-  var args = search.split("&");
-  var cicuri = "-1", theoryuri = "-1", mode = "-1";
-  for (var i = 0 ; i < args.length ; i++) {
-     var couple = args[i].split("=");
-     switch (couple[0]) {
-        case "cicuri"       : cicuri     =couple[1]; break;
-        case "theoryuri"    : theoryuri  =couple[1]; break;
-        case "mode"         : mode       =couple[1]; break;
-     }
-  }
-  if (cicuri == "-1") cicuri = getDefaultParam("cicuri");
-  if (theoryuri == "-1") theoryuri = getDefaultParam("theoryuri");
-  if (mode == "-1") mode = getDefaultParam("mode");
-
-  document.links[2].href =
-   document.links[2].protocol + '//' +
-   document.links[2].host +
-   document.links[2].pathname +
-   "?getterURL=" + getGetterURL();
-
-  document.links[3].href = 
-   document.links[3].protocol + '//' +
-   document.links[3].host +
-   document.links[3].pathname +
-   "?processorURL=" + getUwoboURL() +
-   "&getterURL=" + getGetterURL();
-
-  var topurl =
-   chopSlash(chopSlash(
-    document.location.protocol + '//' +
-    document.location.host +
-    document.location.pathname));
-  document.links[4].href =
-     getUwoboURL() + "apply" +
-      "?keys=RT" +
-      "&param.topurl=" + topurl +
-      "&xmluri=" +
-      escape(
-       topurl + "/html/library/index.html" +
-       "?cicuri=" + cicuri +
-       "&theoryuri=" + theoryuri +
-       "&mode=" + mode +
-       "&processorURL=" + getUwoboURL() +
-       "&getterURL=" + getGetterURL() +
-       "&proofcheckerURL=" + getProofCheckerURL() +
-       "&draw_graphURL=" + getDrawGraphURL() +
-       "&uri_set_queueURL=" + getURISetQueueURL() +
-       "&UNICODEvsSYMBOL=" + getUNICODEvsSYMBOL()
-      );
-}
-
-function selectUwoboURL(ss)
-{
-  if (ss.selectedIndex == 0) {
-    document.uwoboURL.elements[0].value = "";
-  } else {
-    document.uwoboURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":8081/helm/servlet/uwobo/";
-  }
-
-  refreshLinks();
-}
-
-function selectGetterURL(ss)
-{
-  if (ss.selectedIndex == 0) {
-    document.getterURL.elements[0].value = "";
-  } else {
-    document.getterURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":48081/";
-  }
-
-  refreshLinks();
-}
-
-function selectProofCheckerURL(ss)
-{
-  if (ss.selectedIndex == 0) {
-    document.proofcheckerURL.elements[0].value = "";
-  } else {
-    document.proofcheckerURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":48084/";
-  }
-
-  refreshLinks();
-}
-
-function selectDrawGraphURL(ss)
-{
-  if (ss.selectedIndex == 0) {
-    document.draw_graphURL.elements[0].value = "";
-  } else {
-    document.draw_graphURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":48083/";
-  }
-
-  refreshLinks();
-}
-
-function selectURISetQueueURL(ss)
-{
-  if (ss.selectedIndex == 0) {
-    document.uri_set_queueURL.elements[0].value = "";
-  } else {
-    document.uri_set_queueURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":48082/";
-  }
-
-  refreshLinks();
-}