X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fon-line%2Fjavascript%2Futils.js;h=a4ca9cc353e0c0458850f87761d6ee1352fae4fd;hb=7cb90c67bc6f8113188a91ecc29f6db20db5aeb8;hp=7a52b7cbe6d491200ae44cffdede8665ada7ff7f;hpb=97829180b4bc5a72291eeb8156b15b3922f07048;p=helm.git

diff --git a/helm/on-line/javascript/utils.js b/helm/on-line/javascript/utils.js
index 7a52b7cbe..a4ca9cc35 100644
--- a/helm/on-line/javascript/utils.js
+++ b/helm/on-line/javascript/utils.js
@@ -1,12 +1,72 @@
+function dropBodySuffix(url)
+{ var length = url.length;
+  if (url.slice(length - 5, length) == '.body')
+   return (url.slice(0, length - 5));
+  else
+   return url;
+}
+
 function chopSlash(url)
 {
   return url.slice(0,url.lastIndexOf('/'));
 }
 
-function getParam(name)
+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 search = location.search;
-  search = search.slice(1);
   var args = search.split("&");
   var value = "???";
 
@@ -20,6 +80,23 @@ function getParam(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 + "\" ");