]> matita.cs.unibo.it Git - helm.git/blob - helm/uwobo-panel/control.js
ocaml 3.09 transition
[helm.git] / helm / uwobo-panel / control.js
1
2 function getParam(name, def)
3 {
4   var search = top.location.search;
5   search = search.slice(1);
6   var args = search.split("&");
7   var value = "-1";
8   for (var i = 0 ; i < args.length ; i++) {
9     var couple = args[i].split("=");
10     if (couple[0] == name) value = couple[1];
11   }
12   if (value == "-1") value = def;
13   return value;
14 }
15
16 function getInitialPort()
17 {
18   return "38080";
19 }
20
21 function getInitialProcessorURL()
22 {
23   return getParam("processorURL", "http://mowgli.cs.unibo.it:58080/");
24 }
25
26 function getInitialGetterURL()
27 {
28   return getParam("getterURL", "http://mowgli.cs.unibo.it:58081/");
29 }
30
31 function getUwoboURL()
32 {
33   return document.uwoboURL.elements[0].value;
34 }
35
36 function getGetterURL()
37 {
38   return document.getterURL.elements[0].value;
39 }
40
41 function selectUwoboURL(ss)
42 {
43   if (ss.selectedIndex == 0) {
44     document.uwoboURL.elements[0].value = "";
45   } else {
46     document.uwoboURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":58080/";
47   }
48 }
49
50 function selectGetterURL(ss)
51 {
52   if (ss.selectedIndex == 0) {
53     document.getterURL.elements[0].value = "";
54   } else {
55     document.getterURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":8081/";
56   }
57 }
58
59 function getPredefinedStylesheetKey(i)
60 {
61   var v = document.predefinedStylesheets.elements[0].options[i].value;
62   var va = v.split(",");
63   return va[0];
64 }
65
66 function getPredefinedStylesheetURI(i)
67 {
68   var v = document.predefinedStylesheets.elements[0].options[i].value;
69   var va = v.split(",");
70   return va[1];
71 }
72
73 function getPredefinedStylesheetUseGetter(i)
74 {
75   var v = document.predefinedStylesheets.elements[0].options[i].value;
76   var va = v.split(",");
77   return va[2];
78 }
79
80 function selectPredefinedStylesheet(ss)
81 {
82   if (ss.selectedIndex == 0) {
83     document.stylesheetURI.elements[0].value = "";
84     document.stylesheetKey.elements[0].value = "";
85   } else {
86     document.stylesheetURI.elements[0].value = getPredefinedStylesheetURI(ss.selectedIndex);
87     document.stylesheetKey.elements[0].value = getPredefinedStylesheetKey(ss.selectedIndex);
88   }
89
90   document.loadUseGetter.elements[0].checked = getPredefinedStylesheetUseGetter(ss.selectedIndex) == "true" ? true : false;
91   document.loadEscape.elements[0].checked = true;
92 }
93
94 function getProfileParams()
95 {
96   var password = document.getParamsProfilePassword.elements[0].value;
97   if (password != "") { password = "&password=" + password; };
98
99   top.result.location.replace(getUwoboURL() + "getparams?id=" + document.getParamsProfileID.elements[0].value + password);
100 }
101
102 function setProfileParam()
103 {
104   var password = document.setParamProfilePassword.elements[0].value;
105   if (password != "") { password = "&password=" + password; };
106
107   top.result.location.replace(getUwoboURL() + "setparam?id=" + document.setParamProfileID.elements[0].value + "&key=" + document.setParamProfileKey.elements[0].value + "&value=" + document.setParamProfileValue.elements[0].value + password);
108 }
109
110 function createProfile()
111 {
112   var id = document.createProfileID.elements[0].value;
113   if (id != "") { id = "&id=" + id; };
114
115   var password = document.createProfilePassword.elements[0].value;
116   if (password != "") { password = "&password=" + password; };
117
118   var clone = document.createProfileClone.elements[0].value;
119   if (clone != "") { clone = "&orig=" + clone; };
120
121   top.result.location.replace(getUwoboURL() + "createprofile?foo=x" + id + password + clone);
122 }
123
124 function removeProfile()
125 {
126   var password = document.removeProfilePassword.elements[0].value;
127   if (password != "") { password = "&password=" + password; };
128
129   top.result.location.replace(getUwoboURL() + "removeprofile?id=" + document.removeProfileID.elements[0].value + password);
130 }
131
132 function getStylesheetURL()
133 {
134   var s;
135
136   if (document.loadUseGetter.elements[0].checked) {
137     s = getGetterURL() + "getxslt?uri=" + document.stylesheetURI.elements[0].value;
138   } else {
139     s = document.stylesheetURI.elements[0].value;
140   }
141
142   if (document.loadEscape.elements[0].checked) s = escape(s);
143   
144   return s;
145 }
146
147 function loadStylesheet()
148 {
149   top.result.location.replace(getUwoboURL() + "add?bind=" + document.stylesheetKey.elements[0].value + "," + getStylesheetURL());
150 }
151
152 function removeStylesheet()
153 {
154   top.result.location.replace(getUwoboURL() + "remove?keys=" + document.stylesheetKey.elements[0].value);
155 }
156
157 function removeAllStylesheets()
158 {
159   top.result.location.replace(getUwoboURL() + "remove?keys=");
160 }
161
162 function reloadStylesheet()
163 {
164   top.result.location.replace(getUwoboURL() + "reload?keys=" + document.stylesheetKey.elements[0].value);
165 }
166
167 function reloadAllStylesheets()
168 {
169   top.result.location.replace(getUwoboURL() + 'reload?keys=');
170 }
171
172 function loadAllPredefined()
173 {
174   with (document.predefinedStylesheets.elements[0]) {
175     var i;
176     var request = "";
177
178     for (i = 1; i < length; i++)
179       request +=
180         (request == "" ? "" : "&") +
181         "bind=" + getPredefinedStylesheetKey(i) + "," +  escape((getPredefinedStylesheetUseGetter(i) == "true" ? (getGetterURL() + "getxslt?uri=") : "") + getPredefinedStylesheetURI(i));
182     top.result.location.replace(getUwoboURL() + "add?" + request);
183   }
184 }
185
186 function removeAllPredefined()
187 {
188   with (document.predefinedStylesheets.elements[0]) {
189     var i;
190     var request = "";
191
192     for (i = 1; i < length; i++)
193       request += getPredefinedStylesheetKey(i) + (i == length - 1 ? "" : ",");
194     top.result.location.replace(getUwoboURL() + "remove?keys=" + request);
195   }
196 }
197
198 function applyStylesheets()
199 {
200   var i = 0;
201   var keyList = document.keyList.elements[0].value.split(" ");
202
203   var url = getUwoboURL() + "apply?xmluri=";
204   
205   var sourceURL = "";
206
207   if (document.applyUseGetter.elements[0].checked)
208     sourceURL += getGetterURL() + "getxml?uri=";
209     
210   sourceURL += document.sourceDocument.elements[0].value;
211
212   if (document.escapeSource.elements[0].checked)
213     url += escape(sourceURL);
214   else
215     url += sourceURL;
216
217   url += "&keys=";
218   for (i = 0; i < keyList.length; i++) {
219     url += keyList[i];
220     if (i < keyList.length - 1) url += ",";
221   }
222
223   var paramList = document.parameters.elements[0].value.split(" ");
224   for (i = 0; i < paramList.length; i++)
225     if (paramList[i].length > 0) {
226       if (document.escapeParameters.elements[0].checked) {
227         var p = paramList[i].split("=");
228         url += "&param." + p[0] + "=" + escape(p[1]);
229       } else
230         url += "&param." + paramList[i];
231     }
232   
233   top.result.location.replace(url);
234 }