]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/on-line/javascript/prelude.js
New HELM interface almost stable.
[helm.git] / helm / on-line / javascript / prelude.js
index 83cff42bc5d2541db61bc284aaff3a50a0166093..fc3b2470e51749b0f2553fabb5f3d733321c6f02 100644 (file)
@@ -84,21 +84,26 @@ function getInitialUNICODEvsSYMBOL()
   return UNICODEvsSYMBOL;
 }
 
-function getInitialUNICODEvsSYMBOLsymbol()
+function getInitialUNICODEvsSYMBOLsymbol(defaultValue)
 {
-  if (getInitialUNICODEvsSYMBOL() == "symbol")
+  if (defaultValue == "symbol")
    return "CHECKED";
   else
    return "";
 }
 
-function getInitialUNICODEvsSYMBOLunicode()
+function getInitialUNICODEvsSYMBOLunicode(defaultValue)
 {
-  if (getInitialUNICODEvsSYMBOL() == "unicode")
+  if (defaultValue == "unicode")
    return "CHECKED";
   else
    return "";
 }
+function getProfileId()
+{
+  return document.profile.elements[0].value;
+}
 
 function getUwoboURL()
 {
@@ -125,12 +130,43 @@ function getURISetQueueURL()
   return document.uri_set_queueURL.elements[0].value;
 }
 
+function getRdflyURL()
+{
+  return document.rdflyURL.elements[0].value;
+}
+
 function getUNICODEvsSYMBOL()
 {
   if (document.UNICODEvsSYMBOL.radioUNICODEvsSYMBOL[0].checked)
-   return document.UNICODEvsSYMBOL.radioUNICODEvsSYMBOL[0].value;
+   return 'symbol';
+  else
+   return 'unicode';
+}
+
+function getNaturalLanguage()
+{
+  if (document.naturalLanguage.elements[0].checked)
+   return 'yes';
   else
-   return document.UNICODEvsSYMBOL.radioUNICODEvsSYMBOL[1].value;
+   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.rdflyURL=' + escape(getRdflyURL()) +
+    '&param.naturalLanguage=' + escape(getNaturalLanguage()) +
+    '&param.uri_set_size=' + escape(getMaxGraphSize()) +
+    '&param.UNICODEvsSYMBOL=' + escape(getUNICODEvsSYMBOL());
 }
 
 function chopSlash(url)
@@ -198,10 +234,8 @@ 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/";
+    document.uwoboURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":58080/";
   }
-
-  refreshLinks();
 }
 
 function selectGetterURL(ss)
@@ -209,10 +243,8 @@ 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/";
+    document.getterURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":58081/";
   }
-
-  refreshLinks();
 }
 
 function selectProofCheckerURL(ss)
@@ -220,10 +252,8 @@ 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/";
+    document.proofcheckerURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":58084/";
   }
-
-  refreshLinks();
 }
 
 function selectDrawGraphURL(ss)
@@ -231,10 +261,8 @@ 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/";
+    document.draw_graphURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":58083/";
   }
-
-  refreshLinks();
 }
 
 function selectURISetQueueURL(ss)
@@ -242,8 +270,41 @@ 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/";
+    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 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');
+}
 
-  refreshLinks();
+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();
+  }
 }
+