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