X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fon-line%2Fjavascript%2Futils.js;fp=helm%2Fon-line%2Fjavascript%2Futils.js;h=0000000000000000000000000000000000000000;hb=e108abe5c0b4eb841c4ad332229a6c0e57e70079;hp=bb018ad0edee4cd57d1485bbf06a3a2b912eee61;hpb=1456c337a60f6677ee742ff7891d43fc382359a9;p=helm.git

diff --git a/helm/on-line/javascript/utils.js b/helm/on-line/javascript/utils.js
deleted file mode 100644
index bb018ad0e..000000000
--- a/helm/on-line/javascript/utils.js
+++ /dev/null
@@ -1,105 +0,0 @@
-function chopSlash(url)
-{
-  return url.slice(0,url.lastIndexOf('/'));
-}
-
-function dropParam(url,name)
-{
-  var urla = url.split("?");
-  var search = urla[1];
-  var args = search.split("&");
-  var newargs = new Array();
-  var j = 0;
-
-  for (var i = 0 ; i < args.length ; i++) {
-     var couple = args[i].split("=");
-     if (couple[0] != name) {
-        newargs[j] = args[i];
-        j++;
-     }
-  }
-
-  return (urla[0] + "?" + newargs.join("&"));
-}
-
-function setParam(url,name,value)
-{
-  var urla = url.split("?");
-  var search = urla[1];
-  var args = search.split("&");
-  var found = false;
-
-  for (var i = 0 ; i < args.length ; i++) {
-     var couple = args[i].split("=");
-     if (couple[0] == name) {
-        found = true;
-        args[i] = name + "=" + value;
-     }
-  }
-
-  return (urla[0] + "?" + args.join("&") + (found ? "" : ("&" + name + "=" + value)));
-}
-
-function extractParam(url,name)
-{
-  var search = url.split("?")[1];
-  search = search.split("#")[0];
-  var args = search.split("&");
-  var value = "???";
-
-  for (var i = 0 ; i < args.length ; i++) {
-     var couple = args[i].split("=");
-     if (couple[0] == name) value = couple[1];
-  }
-
-  if (value == "???") value = getDefaultParam(name);
-
-  return value;
-}
-
-function getParam0(search,name)
-{
-  var args = search.split("&");
-  var value = "???";
-
-  for (var i = 0 ; i < args.length ; i++) {
-     var couple = args[i].split("=");
-     if (couple[0] == name) value = couple[1];
-  }
-
-  if (value == "???") value = getDefaultParam(name);
-
-  return value;
-}
-
-function getParam(name)
-{
-  return getParam0(location.search.slice(1),name);
-}
-
-function getParam2(name)
-{
-  var url = unescape(getParam('xmluri'));
-  var tmp = url.split("?");
-
-  if (tmp.length > 1)
-     return getParam0(tmp[1],name);
-  else
-     return getDefaultParam(name);
-}
-
-
-function outputOption(doc, value, content, selected)
-{
-  doc.write("<option value=\"" + value + "\" ");
-  if (value == selected) doc.write("selected ");
-  doc.write(">" + content + "</option>");
-}
-
-function outputCheckbox(doc, onclick, content, checked)
-{
-  doc.write("<input type=\"checkbox\" onClick=\"" + onclick + "\" ");
-  if (checked) doc.write("checked");
-  doc.write(">" + content + "</input>");
-}
-