]> matita.cs.unibo.it Git - helm.git/blob - helm/on-line/javascript/utils.js
a4ca9cc353e0c0458850f87761d6ee1352fae4fd
[helm.git] / helm / on-line / javascript / utils.js
1 function dropBodySuffix(url)
2 { var length = url.length;
3   if (url.slice(length - 5, length) == '.body')
4    return (url.slice(0, length - 5));
5   else
6    return url;
7 }
8
9 function chopSlash(url)
10 {
11   return url.slice(0,url.lastIndexOf('/'));
12 }
13
14 function dropParam(url,name)
15 {
16   var urla = url.split("?");
17   var search = urla[1];
18   var args = search.split("&");
19   var newargs = new Array();
20   var j = 0;
21
22   for (var i = 0 ; i < args.length ; i++) {
23      var couple = args[i].split("=");
24      if (couple[0] != name) {
25         newargs[j] = args[i];
26         j++;
27      }
28   }
29
30   return (urla[0] + "?" + newargs.join("&"));
31 }
32
33 function setParam(url,name,value)
34 {
35   var urla = url.split("?");
36   var search = urla[1];
37   var args = search.split("&");
38   var found = false;
39
40   for (var i = 0 ; i < args.length ; i++) {
41      var couple = args[i].split("=");
42      if (couple[0] == name) {
43         found = true;
44         args[i] = name + "=" + value;
45      }
46   }
47
48   return (urla[0] + "?" + args.join("&") + (found ? "" : ("&" + name + "=" + value)));
49 }
50
51 function extractParam(url,name)
52 {
53   var search = url.split("?")[1];
54   search = search.split("#")[0];
55   var args = search.split("&");
56   var value = "???";
57
58   for (var i = 0 ; i < args.length ; i++) {
59      var couple = args[i].split("=");
60      if (couple[0] == name) value = couple[1];
61   }
62
63   if (value == "???") value = getDefaultParam(name);
64
65   return value;
66 }
67
68 function getParam0(search,name)
69 {
70   var args = search.split("&");
71   var value = "???";
72
73   for (var i = 0 ; i < args.length ; i++) {
74      var couple = args[i].split("=");
75      if (couple[0] == name) value = couple[1];
76   }
77
78   if (value == "???") value = getDefaultParam(name);
79
80   return value;
81 }
82
83 function getParam(name)
84 {
85   return getParam0(location.search.slice(1),name);
86 }
87
88 function getParam2(name)
89 {
90   var url = unescape(getParam('xmluri'));
91   var tmp = url.split("?");
92
93   if (tmp.length > 1)
94      return getParam0(tmp[1],name);
95   else
96      return getDefaultParam(name);
97 }
98
99
100 function outputOption(doc, value, content, selected)
101 {
102   doc.write("<option value=\"" + value + "\" ");
103   if (value == selected) doc.write("selected ");
104   doc.write(">" + content + "</option>");
105 }
106
107 function outputCheckbox(doc, onclick, content, checked)
108 {
109   doc.write("<input type=\"checkbox\" onClick=\"" + onclick + "\" ");
110   if (checked) doc.write("checked");
111   doc.write(">" + content + "</input>");
112 }
113