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