X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Fon-line%2Fjavascript%2Futils.js;fp=helm%2Fon-line%2Fjavascript%2Futils.js;h=0000000000000000000000000000000000000000;hp=a4ca9cc353e0c0458850f87761d6ee1352fae4fd;hb=3ef089a4c58fbe429dd539af6215991ecbe11ee2;hpb=1c7fb836e2af4f2f3d18afd0396701f2094265ff
diff --git a/helm/on-line/javascript/utils.js b/helm/on-line/javascript/utils.js
deleted file mode 100644
index a4ca9cc35..000000000
--- a/helm/on-line/javascript/utils.js
+++ /dev/null
@@ -1,113 +0,0 @@
-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 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("");
-}
-
-function outputCheckbox(doc, onclick, content, checked)
-{
- doc.write("" + content + "");
-}
-