]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/on-line/javascript/prelude.js
...
[helm.git] / helm / on-line / javascript / prelude.js
index 69479641cd5af9ee32d8ae20aa3d678ee60df6d6..f319735038448a6d956367e7a2eaba9871329d13 100644 (file)
@@ -27,6 +27,34 @@ function getInitialGetterURL()
   return getterURL;
 }
 
+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;
@@ -67,6 +95,16 @@ function getGetterURL()
   return document.getterURL.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)
@@ -128,6 +166,8 @@ function refreshLinks()
        "&mode=" + mode +
        "&processorURL=" + getUwoboURL() +
        "&getterURL=" + getGetterURL() +
+       "&draw_graphURL=" + getDrawGraphURL() +
+       "&uri_set_queueURL=" + getURISetQueueURL() +
        "&UNICODEvsSYMBOL=" + getUNICODEvsSYMBOL()
       );
 }
@@ -153,3 +193,25 @@ function selectGetterURL(ss)
 
   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 + ":8083/";
+  }
+
+  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 + ":8084/";
+  }
+
+  refreshLinks();
+}