]> matita.cs.unibo.it Git - helm.git/blob - helm/on-line/javascript/utils.js
d7903ef6226d0cccfe9628751b2e6b20de5f0eb7
[helm.git] / helm / on-line / javascript / utils.js
1 function chopSlash(url)
2 {
3   return url.slice(0,url.lastIndexOf('/'));
4 }
5
6 function setParam(url,name,value)
7 {
8   var urla = url.split("?");
9   var search = urla[1];
10   var args = search.split("&");
11
12   for (var i = 0 ; i < args.length ; i++) {
13      var couple = args[i].split("=");
14      if (couple[0] == name) args[i] = name + "=" + value;
15   }
16
17
18   return (urla[0] + "?" + args.join("&"));
19 }
20
21 function extractParam(url,name)
22 {
23   var search = url.split("?")[1];
24   search = search.split("#")[0];
25   var args = search.split("&");
26   var value = "???";
27
28   for (var i = 0 ; i < args.length ; i++) {
29      var couple = args[i].split("=");
30      if (couple[0] == name) value = couple[1];
31   }
32
33   if (value == "???") value = getDefaultParam(name);
34
35   return value;
36 }
37
38 function getParam0(search,name)
39 {
40   var args = search.split("&");
41   var value = "???";
42
43   for (var i = 0 ; i < args.length ; i++) {
44      var couple = args[i].split("=");
45      if (couple[0] == name) value = couple[1];
46   }
47
48   if (value == "???") value = getDefaultParam(name);
49
50   return value;
51 }
52
53 function getParam(name)
54 {
55   return getParam0(location.search.slice(1),name);
56 }
57
58 function getParam2(name)
59 {
60   var url = unescape(getParam('xmluri'));
61   var tmp = url.split("?");
62
63   if (tmp.length > 1)
64      return getParam0(tmp[1],name);
65   else
66      return getDefaultParam(name);
67 }
68
69
70 function outputOption(doc, value, content, selected)
71 {
72   doc.write("<option value=\"" + value + "\" ");
73   if (value == selected) doc.write("selected ");
74   doc.write(">" + content + "</option>");
75 }
76
77 function outputCheckbox(doc, onclick, content, checked)
78 {
79   doc.write("<input type=\"checkbox\" onClick=\"" + onclick + "\" ");
80   if (checked) doc.write("checked");
81   doc.write(">" + content + "</input>");
82 }
83