X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fon-line%2Fjavascript%2Fprelude.js;h=d89ae566d333ae2b54a70c88f8adec07c2697ade;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;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..d89ae566d 100644
--- a/helm/on-line/javascript/prelude.js
+++ b/helm/on-line/javascript/prelude.js
@@ -1,30 +1,6 @@
-
-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()
+function getProfileId()
 {
-  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;
+  return document.profile.elements[0].value;
 }
 
 function getUwoboURL()
@@ -37,35 +13,70 @@ function getGetterURL()
   return document.getterURL.elements[0].value;
 }
 
-function refreshLinks()
+function getProofCheckerURL()
 {
-  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"    : theoryicuri  =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");
+  return document.proofcheckerURL.elements[0].value;
+}
+
+function getSearchEngineURL()
+{
+  return document.searchengineURL.elements[0].value;
+}
+
+function getDrawGraphURL()
+{
+  return document.draw_graphURL.elements[0].value;
+}
+
+function getURISetQueueURL()
+{
+  return document.uri_set_queueURL.elements[0].value;
+}
 
-  document.links[2].search = "?getterURL=" + getGetterURL();
-  
-  document.links[3].search = 
-    "?processorURL=" + getUwoboURL() +
-    "&getterURL=" + getGetterURL();
+function getRdflyURL()
+{
+  return document.rdflyURL.elements[0].value;
+}
 
-  document.links[4].href = "../html/library/index.html?cicuri=" + cicuri
-     + "&theoryuri=" + theoryuri
-     + "&mode=" + mode
-     + "&processorURL=" + getUwoboURL()
-     + "&getterURL=" + getGetterURL();
+function getInterfaceURL()
+{
+  return document.interfaceURL.elements[0].value;
+}
+
+function getUNICODEvsSYMBOL()
+{
+  if (document.UNICODEvsSYMBOL.radioUNICODEvsSYMBOL[0].checked)
+   return 'symbol';
+  else
+   return 'unicode';
+}
+
+function getNaturalLanguage()
+{
+  if (document.naturalLanguage.elements[0].checked)
+   return 'yes';
+  else
+   return 'no';
+}
+
+function getMaxGraphSize()
+{
+  return document.maxGraphSize.elements[0].value;
+}
+
+function getUpdateURL()
+{
+  return '&param.processorURL=' + escape(getUwoboURL()) +
+    '&param.getterURL=' + escape(getGetterURL()) +
+    '&param.uri_set_queueURL=' + escape(getURISetQueueURL()) +
+    '&param.draw_graphURL=' + escape(getDrawGraphURL()) +
+    '&param.proofcheckerURL=' + escape(getProofCheckerURL()) +
+    '&param.searchengineURL=' + escape(getSearchEngineURL()) +
+    '&param.rdflyURL=' + escape(getRdflyURL()) +
+    '&param.interfaceURL=' + escape(getInterfaceURL()) +
+    '&param.naturalLanguage=' + escape(getNaturalLanguage()) +
+    '&param.uri_set_size=' + escape(getMaxGraphSize()) +
+    '&param.UNICODEvsSYMBOL=' + escape(getUNICODEvsSYMBOL());
 }
 
 function selectUwoboURL(ss)
@@ -73,19 +84,95 @@ 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 + ":58080/";
   }
-
-  refreshLink();
 }
-
+                                                                                
 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 + ":58081/";
+  }
+}
+
+function selectProofCheckerURL(ss)
+{
+  if (ss.selectedIndex == 0) {
+    document.proofcheckerURL.elements[0].value = "";
+  } else {
+    document.proofcheckerURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":58084/";
+  }
+}
+
+function selectSearchEngineURL(ss)
+{
+  if (ss.selectedIndex == 0) {
+    document.searchengineURL.elements[0].value = "";
+  } else {
+    document.searchengineURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":58085/";
+  }
+}
+
+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 + ":58083/";
   }
+}
 
-  refreshLink();
+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 + ":58082/";
+  }
 }
+
+function selectRdflyURL(ss)
+{
+  if (ss.selectedIndex == 0) {
+    document.rdflyURL.elements[0].value = "";
+  } else {
+    document.rdflyURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":58086/";
+  }
+}
+
+function selectInterfaceURL(ss)
+{
+  if (ss.selectedIndex == 0) {
+    document.interfaceURL.elements[0].value = "";
+  } else {
+    document.interfaceURL.elements[0].value = "http://helm.cs.unibo.it/helm";
+  }
+}
+
+function selectProfile(ss, interfaceURL)
+{
+  location = getUwoboURL() +
+    'apply?keys=SPK&param.processorURL=' + escape(getUwoboURL()) +
+    '&param.profile=' + escape(ss.options[ss.selectedIndex].value) +
+    '&xmluri=' + escape(interfaceURL + 'html/configuration.html');
+}
+
+function saveProfile(origProfileId)
+{
+  var profileId = getProfileId();
+  var exists = false;
+  var i;
+  var options = document.profileList.elements[0];
+  for (i = 0; i < options.length; i++)
+    if (profileId == options[i].value) exists = true;
+  if (exists) {
+    if (confirm('Update the profile \'' + profileId + '\'?'))
+      location = getUwoboURL() + 'setparams?id=' + profileId + getUpdateURL();
+  } else {
+    if (confirm('Create a new profile \'' + profileId + '\' with the current settings?'))
+      location = getUwoboURL() + 'createprofile?id=' + profileId + '&orig=' + origProfileId + getUpdateURL();
+  }
+}
+