]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/uwobo-panel/control.js
daemons tamed
[helm.git] / helm / uwobo-panel / control.js
diff --git a/helm/uwobo-panel/control.js b/helm/uwobo-panel/control.js
deleted file mode 100644 (file)
index 9858fe1..0000000
+++ /dev/null
@@ -1,234 +0,0 @@
-
-function getParam(name, def)
-{
-  var search = top.location.search;
-  search = search.slice(1);
-  var args = search.split("&");
-  var value = "-1";
-  for (var i = 0 ; i < args.length ; i++) {
-    var couple = args[i].split("=");
-    if (couple[0] == name) value = couple[1];
-  }
-  if (value == "-1") value = def;
-  return value;
-}
-
-function getInitialPort()
-{
-  return "38080";
-}
-
-function getInitialProcessorURL()
-{
-  return getParam("processorURL", "http://mowgli.cs.unibo.it:58080/");
-}
-
-function getInitialGetterURL()
-{
-  return getParam("getterURL", "http://mowgli.cs.unibo.it:58081/");
-}
-
-function getUwoboURL()
-{
-  return document.uwoboURL.elements[0].value;
-}
-
-function getGetterURL()
-{
-  return document.getterURL.elements[0].value;
-}
-
-function selectUwoboURL(ss)
-{
-  if (ss.selectedIndex == 0) {
-    document.uwoboURL.elements[0].value = "";
-  } else {
-    document.uwoboURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":58080/";
-  }
-}
-
-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/";
-  }
-}
-
-function getPredefinedStylesheetKey(i)
-{
-  var v = document.predefinedStylesheets.elements[0].options[i].value;
-  var va = v.split(",");
-  return va[0];
-}
-
-function getPredefinedStylesheetURI(i)
-{
-  var v = document.predefinedStylesheets.elements[0].options[i].value;
-  var va = v.split(",");
-  return va[1];
-}
-
-function getPredefinedStylesheetUseGetter(i)
-{
-  var v = document.predefinedStylesheets.elements[0].options[i].value;
-  var va = v.split(",");
-  return va[2];
-}
-
-function selectPredefinedStylesheet(ss)
-{
-  if (ss.selectedIndex == 0) {
-    document.stylesheetURI.elements[0].value = "";
-    document.stylesheetKey.elements[0].value = "";
-  } else {
-    document.stylesheetURI.elements[0].value = getPredefinedStylesheetURI(ss.selectedIndex);
-    document.stylesheetKey.elements[0].value = getPredefinedStylesheetKey(ss.selectedIndex);
-  }
-
-  document.loadUseGetter.elements[0].checked = getPredefinedStylesheetUseGetter(ss.selectedIndex) == "true" ? true : false;
-  document.loadEscape.elements[0].checked = true;
-}
-
-function getProfileParams()
-{
-  var password = document.getParamsProfilePassword.elements[0].value;
-  if (password != "") { password = "&password=" + password; };
-
-  top.result.location.replace(getUwoboURL() + "getparams?id=" + document.getParamsProfileID.elements[0].value + password);
-}
-
-function setProfileParam()
-{
-  var password = document.setParamProfilePassword.elements[0].value;
-  if (password != "") { password = "&password=" + password; };
-
-  top.result.location.replace(getUwoboURL() + "setparam?id=" + document.setParamProfileID.elements[0].value + "&key=" + document.setParamProfileKey.elements[0].value + "&value=" + document.setParamProfileValue.elements[0].value + password);
-}
-
-function createProfile()
-{
-  var id = document.createProfileID.elements[0].value;
-  if (id != "") { id = "&id=" + id; };
-
-  var password = document.createProfilePassword.elements[0].value;
-  if (password != "") { password = "&password=" + password; };
-
-  var clone = document.createProfileClone.elements[0].value;
-  if (clone != "") { clone = "&orig=" + clone; };
-
-  top.result.location.replace(getUwoboURL() + "createprofile?foo=x" + id + password + clone);
-}
-
-function removeProfile()
-{
-  var password = document.removeProfilePassword.elements[0].value;
-  if (password != "") { password = "&password=" + password; };
-
-  top.result.location.replace(getUwoboURL() + "removeprofile?id=" + document.removeProfileID.elements[0].value + password);
-}
-
-function getStylesheetURL()
-{
-  var s;
-
-  if (document.loadUseGetter.elements[0].checked) {
-    s = getGetterURL() + "getxslt?uri=" + document.stylesheetURI.elements[0].value;
-  } else {
-    s = document.stylesheetURI.elements[0].value;
-  }
-
-  if (document.loadEscape.elements[0].checked) s = escape(s);
-  
-  return s;
-}
-
-function loadStylesheet()
-{
-  top.result.location.replace(getUwoboURL() + "add?bind=" + document.stylesheetKey.elements[0].value + "," + getStylesheetURL());
-}
-
-function removeStylesheet()
-{
-  top.result.location.replace(getUwoboURL() + "remove?keys=" + document.stylesheetKey.elements[0].value);
-}
-
-function removeAllStylesheets()
-{
-  top.result.location.replace(getUwoboURL() + "remove?keys=");
-}
-
-function reloadStylesheet()
-{
-  top.result.location.replace(getUwoboURL() + "reload?keys=" + document.stylesheetKey.elements[0].value);
-}
-
-function reloadAllStylesheets()
-{
-  top.result.location.replace(getUwoboURL() + 'reload?keys=');
-}
-
-function loadAllPredefined()
-{
-  with (document.predefinedStylesheets.elements[0]) {
-    var i;
-    var request = "";
-
-    for (i = 1; i < length; i++)
-      request +=
-        (request == "" ? "" : "&") +
-        "bind=" + getPredefinedStylesheetKey(i) + "," +  escape((getPredefinedStylesheetUseGetter(i) == "true" ? (getGetterURL() + "getxslt?uri=") : "") + getPredefinedStylesheetURI(i));
-    top.result.location.replace(getUwoboURL() + "add?" + request);
-  }
-}
-
-function removeAllPredefined()
-{
-  with (document.predefinedStylesheets.elements[0]) {
-    var i;
-    var request = "";
-
-    for (i = 1; i < length; i++)
-      request += getPredefinedStylesheetKey(i) + (i == length - 1 ? "" : ",");
-    top.result.location.replace(getUwoboURL() + "remove?keys=" + request);
-  }
-}
-
-function applyStylesheets()
-{
-  var i = 0;
-  var keyList = document.keyList.elements[0].value.split(" ");
-
-  var url = getUwoboURL() + "apply?xmluri=";
-  
-  var sourceURL = "";
-
-  if (document.applyUseGetter.elements[0].checked)
-    sourceURL += getGetterURL() + "getxml?uri=";
-    
-  sourceURL += document.sourceDocument.elements[0].value;
-
-  if (document.escapeSource.elements[0].checked)
-    url += escape(sourceURL);
-  else
-    url += sourceURL;
-
-  url += "&keys=";
-  for (i = 0; i < keyList.length; i++) {
-    url += keyList[i];
-    if (i < keyList.length - 1) url += ",";
-  }
-
-  var paramList = document.parameters.elements[0].value.split(" ");
-  for (i = 0; i < paramList.length; i++)
-    if (paramList[i].length > 0) {
-      if (document.escapeParameters.elements[0].checked) {
-        var p = paramList[i].split("=");
-        url += "&param." + p[0] + "=" + escape(p[1]);
-      } else
-        url += "&param." + paramList[i];
-    }
-  
-  top.result.location.replace(url);
-}