X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fon-line%2Fjavascript%2Fprelude.js;h=83cff42bc5d2541db61bc284aaff3a50a0166093;hb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1;hp=dff8c31fa0ae580a235d8de6ad20940ffb2594ee;hpb=97829180b4bc5a72291eeb8156b15b3922f07048;p=helm.git

diff --git a/helm/on-line/javascript/prelude.js b/helm/on-line/javascript/prelude.js
index dff8c31fa..83cff42bc 100644
--- a/helm/on-line/javascript/prelude.js
+++ b/helm/on-line/javascript/prelude.js
@@ -27,6 +27,79 @@ function getInitialGetterURL()
   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;
@@ -37,6 +110,34 @@ 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;
@@ -46,26 +147,50 @@ function refreshLinks()
   for (var i = 0 ; i < args.length ; i++) {
      var couple = args[i].split("=");
      switch (couple[0]) {
-        case "cicuri"       : cicuri       =couple[1]; break;
-        case "theoryuri"    : theoryicuri  =couple[1]; break;
-        case "mode"         : mode         =couple[1]; break;
+        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].search = "?getterURL=" + getGetterURL();
-  
-  document.links[3].search = 
-    "?processorURL=" + getUwoboURL() +
-    "&getterURL=" + getGetterURL();
+  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();
 
-  document.links[4].href = "../html/library/index.html?cicuri=" + cicuri
-     + "&theoryuri=" + theoryuri
-     + "&mode=" + mode
-     + "&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)
@@ -73,10 +198,10 @@ function selectUwoboURL(ss)
   if (ss.selectedIndex == 0) {
     document.uwoboURL.elements[0].value = "";
   } else {
-    document.uwoboURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":8080/helm/servlet/uwobo/";
+    document.uwoboURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":8081/helm/servlet/uwobo/";
   }
 
-  refreshLink();
+  refreshLinks();
 }
 
 function selectGetterURL(ss)
@@ -84,8 +209,41 @@ function selectGetterURL(ss)
   if (ss.selectedIndex == 0) {
     document.getterURL.elements[0].value = "";
   } else {
-    document.getterURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":8081/";
+    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/";
   }
 
-  refreshLink();
+  refreshLinks();
 }