]> matita.cs.unibo.it Git - helm.git/blob - helm/on-line/javascript/control.js
added http_client module
[helm.git] / helm / on-line / javascript / control.js
1 function updateMode(i, s)
2 {
3   var mode = top.mode;
4   var mode_list = mode.split(",");
5   var res = "";
6   var j;
7
8   for (j = 0; j < mode_list.length; j++) {
9     if (j == i) res += s;
10     else res += mode_list[j];
11     if (j < mode_list.length - 1) res += ",";
12   }
13   
14   top.mode = res;
15 }
16
17 function updateOutput(output,format)
18 {
19   var theoryuri = top.theoryuri;
20   var cicuri = top.cicuri;
21   var mode = top.mode;
22   var topurl = top.topurl;
23   var processorURL = top.processorURL;
24   var getterURL = top.getterURL;
25   var proofcheckerURL = top.proofcheckerURL;
26   var draw_graphURL = top.draw_graphURL;
27   var uri_set_queueURL = top.uri_set_queueURL;
28   var mode_list = mode.split(",");
29   var new_mode = output.options[output.selectedIndex].value;
30   var dest = "?theoryuri=" + theoryuri + "&cicuri=" + cicuri + "&topurl=" + topurl + "&processorURL=" + processorURL + "&getterURL=" + getterURL + "&proofcheckerURL=" + proofcheckerURL + "&draw_graphURL=" + draw_graphURL + "&uri_set_queueURL=" + uri_set_queueURL + "&mode=";
31   
32   if (new_mode != mode_list[0]) {
33     updateMode(0, new_mode);
34     if (new_mode == "raw") updateMode(2, format.options[format.selectedIndex].value);
35     else updateMode(1, format.options[format.selectedIndex].value);
36
37     var href =
38      top.processorURL + 'apply' +
39      '?keys=RT' +
40      '&param.topurl=' + topurl +
41      '&xmluri=' +
42      escape(top.topurl + '/html/library/control.html' + dest + top.mode);
43     
44     location.href = href;
45   }
46 }
47
48 function updateFormat(format)
49 {
50   var mode = top.mode;
51   var mode_list = mode.split(",");
52
53   if (mode_list[0] == "raw") {
54     updateMode(1, format.options[format.selectedIndex].value);
55   } else {
56     updateMode(2, format.options[format.selectedIndex].value);
57   }
58
59   refreshReload();
60 }
61
62 function updateNatural(checkbox)
63 {
64   if (checkbox.checked) updateMode(3, "yes");
65   else updateMode(3, "no");
66   refreshReload();
67 }
68
69 function updateAnnotations(checkbox)
70 {
71   if (checkbox.checked) updateMode(4, "yes");
72   else updateMode(4, "no");
73   refreshReload();
74 }
75
76 function updateCompressed(checkbox)
77 {
78   if (checkbox.checked) updateMode(5, "gz");
79   else updateMode(5, "normal");
80   refreshReload();
81 }
82
83 function updateDTDPatched(checkbox)
84 {
85   if (checkbox.checked) updateMode(6, "yes");
86   else updateMode(6, "no");
87   refreshReload();
88 }
89
90 function refreshReload()
91 {
92    var search = 
93       "?mode=" + top.mode +
94       "&cicuri=" + top.cicuri +
95       "&theoryuri=" + top.theoryuri +
96       "&processorURL=" + top.processorURL +
97       "&getterURL=" + top.getterURL +
98       "&proofcheckerURL=" + top.proofcheckerURL +
99       "&draw_graphURL=" + top.draw_graphURL +
100       "&uri_set_queueURL=" + top.uri_set_queueURL +
101       "&UNICODEvsSYMBOL=" + top.UNICODEvsSYMBOL;
102
103    var href =
104     top.processorURL + 'apply' +
105     '?keys=RT' +
106     '&param.topurl=' + top.topurl +
107     '&xmluri=' +
108     escape(top.topurl + '/html/library/index.html' + search);
109     
110    top.frames[0].document.links[0].href = href;
111    top.frames[0].document.links[1].href =
112     top.topurl + '/html/index.html' + search;
113
114    return true;
115 }
116
117 function refreshcicHeader(headerURL)
118 {
119    top.cicheader.location.search = "?keys=GP&xmluri=" + headerURL + "&param.uri=" + top.cicuri;
120    return true;
121 }
122
123 function refreshtheoryHeader(headerURL)
124 {
125    top.theoryheader.location.search = "?keys=GP&xmluri=" + headerURL + "&param.uri=" + top.theoryuri;
126    return true;
127 }
128
129 function getCICMathMLKeys()
130 {
131   return escape("d_c,C1,G,C2,L");
132 }
133
134 function getTheoryKeys()
135 {
136   return escape("T1,T2,L,E");
137 }
138
139 function getEmbedKeys()
140 {
141   return escape("d_c,TC1,HC2,L");
142 }
143
144 function getCICHTMLKeys()
145 {
146   return escape("d_c,C1,HC2,L");
147 }
148
149 function getCICProofTreeXHTMLMathMLKeys()
150 {
151   return escape("HAT,G,HAO,L");
152 }
153
154 function makeURL(type,uri,cicflags,typesflags)
155 {
156   var mode = top.mode;
157   var processorURL = top.processorURL;
158   var getterURL = top.getterURL;
159   var proofcheckerURL = top.proofcheckerURL;
160   var draw_graphURL = top.draw_graphURL;
161   var uri_set_queueURL = top.uri_set_queueURL;
162   var UNICODEvsSYMBOL = top.UNICODEvsSYMBOL;
163   var mode_list = mode.split(",");
164   
165   var keys = "";
166   var url = "";
167
168   var interfaceURL = top.topurl + "/html/cic/index.html";
169   var thinterfaceURL = top.topurl + "/html/theory/index.html";
170
171   var output = mode_list[0];
172   var format;
173   if (output == "raw") format = mode_list[1];
174   else format = mode_list[2];
175   
176   if (output == "raw") {
177     var ext = "";
178     var rdfprefix = "";
179     if (format == "types") ext = ".types"
180     else if (format == "ann") ext = ".ann"
181     else if (format == "fwd") rdfprefix = "helm:rdf:www.cs.unibo.it/helm/rdf/forward//"
182     else if (format == "bwd") rdfprefix = "helm:rdf:www.cs.unibo.it/helm/rdf/backward//";
183     url = getterURL + "getxml?uri=" + rdfprefix + uri + ext + "&format=" +
184           mode_list[5] + "&patch_dtd=" + mode_list[6];
185   } else {
186     var uri_len = uri.length;
187     if (format == "html" && type == "cic" && uri.substring(uri.length - 10, uri.length) == "proof_tree") {
188       keys = getCICProofTreeXHTMLMathMLKeys() +
189        "&param.processorURL=" + escape(processorURL) +
190        "&param.getterURL=" + escape(getterURL) +
191        "&param.proofcheckerURL=" + escape(proofcheckerURL) +
192        "&param.draw_graphURL=" + escape(draw_graphURL) +
193        "&param.uri_set_queueURL=" + escape(uri_set_queueURL) +
194        "&param.UNICODEvsSYMBOL=" + escape(UNICODEvsSYMBOL) +
195        "&prop.doctype-public="+escape("-//W3C//DTD XHTML 1.1 plus MathML 2.0//EN")+
196        "&prop.doctype-system="+escape("http://www.w3.org/TR/MathML2/dtd/xhtml-math11-f.dtd")+
197        "&prop.encoding=iso-8859-1" +
198        "&prop.media-type=text/xml" +
199        "&prop.method=xml" +
200        "&param.doctype-public="+escape("-//W3C//DTD XHTML 1.0 Transitional//EN")+
201        "&param.encoding=iso-8859-1" +
202        "&param.media-type=text/html" +
203        "&param.keys=" + getCICHTMLKeys() +
204        "&param.interfaceURL=" + escape(interfaceURL) +
205        "&param.framewidth=150";
206     } else if (format == "html" && type == "cic") {
207       keys = getCICHTMLKeys() +
208        "&param.processorURL=" + escape(processorURL) +
209        "&param.getterURL=" + escape(getterURL) +
210        "&param.proofcheckerURL=" + escape(proofcheckerURL) +
211        "&param.draw_graphURL=" + escape(draw_graphURL) +
212        "&param.uri_set_queueURL=" + escape(uri_set_queueURL) +
213        "&param.UNICODEvsSYMBOL=" + escape(UNICODEvsSYMBOL) +
214        "&prop.doctype-public="+escape("-//W3C//DTD XHTML 1.0 Transitional//EN")+
215        "&prop.encoding=iso-8859-1" +
216        "&prop.media-type=text/html" +
217        "&prop.method=html" +
218        "&param.doctype-public="+escape("-//W3C//DTD XHTML 1.0 Transitional//EN")+
219        "&param.encoding=iso-8859-1" +
220        "&param.media-type=text/html" +
221        "&param.keys=" + getCICHTMLKeys() +
222        "&param.interfaceURL=" + escape(interfaceURL);
223     } else if (format == "html" && type == "theory") {
224       keys = getTheoryKeys()+
225        "&param.processorURL=" + escape(processorURL) +
226        "&param.getterURL=" + escape(getterURL) +
227        "&param.proofcheckerURL=" + escape(proofcheckerURL) +
228        "&param.draw_graphURL=" + escape(draw_graphURL) +
229        "&param.uri_set_queueURL=" + escape(uri_set_queueURL) +
230        "&param.UNICODEvsSYMBOL=" + escape(UNICODEvsSYMBOL) +
231        "&param.keys=" + getCICHTMLKeys() +
232        "&param.thkeys=" + getTheoryKeys() +
233        "&param.embedkeys=" + getEmbedKeys() +
234        "&param.doctype-public="+escape("-//W3C//DTD XHTML 1.0 Transitional//EN")+
235        "&param.encoding=iso-8859-1" +
236        "&param.thencoding=iso-8859-1" +
237        "&param.media-type=text/html" +
238        "&param.thmedia-type=text/html" +
239        "&param.interfaceURL=" + escape(interfaceURL) +
240        "&param.thinterfaceURL=" + escape(thinterfaceURL);
241     } else if (format == "mml_cont" && type == "cic") {
242       keys = escape("d_c,C1")+
243        "&param.processorURL=" + escape(processorURL) +
244        "&param.getterURL=" + escape(getterURL) +
245        "&prop.doctype-public="+
246        //"&prop.encoding=" +
247        "&prop.media-type=text/xml" +
248        "&param.doctype-public=" +
249        "&param.encoding=" +
250        "&param.media-type=text/xml";
251     } else if (format == "mml_cont" && type == "theory") {
252       keys = escape("T1,L,E")+
253        "&param.processorURL=" + escape(processorURL) +
254        "&param.getterURL=" + escape(getterURL) +
255        "&param.keys=" + escape("d_c,C1") +
256        "&param.thkeys=T1,L,E" +
257        "&param.embedkeys=" + escape("d_c,TC1") +
258
259        "&param.processorURL=" + escape(processorURL) +
260        "&param.getterURL=" + escape(getterURL) +
261        "&param.proofcheckerURL=" + escape(proofcheckerURL) +
262        "&param.draw_graphURL=" + escape(draw_graphURL) +
263        "&param.uri_set_queueURL=" + escape(uri_set_queueURL) +
264        "&param.doctype-public=" +
265        "&param.encoding=" +
266        "&param.thencoding=iso-8859-1" +
267        "&param.media-type=text/xml" +
268        "&param.thmedia-type=text/html" +
269        "&param.interfaceURL=" + escape(interfaceURL) +
270        "&param.thinterfaceURL=" + escape(thinterfaceURL);
271     } else if (format == "mml_pres" && type == "cic") {
272       keys = getCICMathMLKeys()+
273        "&param.processorURL=" + escape(processorURL) +
274        "&param.getterURL=" + escape(getterURL) +
275        "&param.proofcheckerURL=" + escape(proofcheckerURL) +
276        "&param.draw_graphURL=" + escape(draw_graphURL) +
277        "&param.uri_set_queueURL=" + escape(uri_set_queueURL) +
278        "&prop.doctype-public="+
279        //"&prop.encoding=" +
280        "&prop.media-type=text/xml" +
281        "&param.doctype-public=" +
282        "&param.encoding=" +
283        "&param.media-type=text/xml" +
284        "&param.keys=" + getCICMathMLKeys() +
285        "&param.interfaceURL=" + escape(interfaceURL);
286     } else if (format == "mml_pres" && type == "theory") {
287       keys = getTheoryKeys()+
288        "&param.keys=" + getCICMathMLKeys() +
289        "&param.thkeys=" + getTheoryKeys() +
290        "&param.embedkeys=" + escape("d_c,TC1,G,C2,L") +
291        "&param.processorURL=" + escape(processorURL) +
292        "&param.getterURL=" + escape(getterURL) +
293        "&param.proofcheckerURL=" + escape(proofcheckerURL) +
294        "&param.draw_graphURL=" + escape(draw_graphURL) +
295        "&param.uri_set_queueURL=" + escape(uri_set_queueURL) +
296        "&param.doctype-public=" +
297        "&param.encoding=" +
298        "&param.thencoding=iso-8859-1" +
299        "&param.media-type=text/xml" +
300        "&param.thmedia-type=text/html" +
301        "&param.interfaceURL=" + escape(interfaceURL) +
302        "&param.thinterfaceURL=" + escape(thinterfaceURL);
303     }
304
305     var naturalLanguage = typesflags.toLowerCase();
306     if (typesflags != "NO" || type == "theory") {
307        naturalLanguage = mode_list[3];
308     }
309     var annotations = cicflags.toLowerCase();
310     if (cicflags != "NO" || type == "theory") {
311        annotations = mode_list[4];
312     }
313     url = processorURL + "apply?xmluri=" + escape(getterURL + "getxml?uri=" + uri) + "&keys=" + keys + "&param.CICURI=" + uri + "&param.naturalLanguage=" + naturalLanguage + "&param.annotations=" + annotations + "&param.topurl=" + top.topurl;
314   }
315
316   if (output == "raw")
317    return url;
318   else if (type == "cic")
319    return interfaceURL + "?url=" + escape(url);
320   else if (type == "theory")
321    return thinterfaceURL + "?url=" + escape(url)
322 }
323