]> matita.cs.unibo.it Git - helm.git/blob - helm/on-line/javascript/control.js
Initial revision
[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 makeURL(type,uri,cicflags,typesflags)
150 {
151   var mode = top.mode;
152   var processorURL = top.processorURL;
153   var getterURL = top.getterURL;
154   var proofcheckerURL = top.proofcheckerURL;
155   var draw_graphURL = top.draw_graphURL;
156   var uri_set_queueURL = top.uri_set_queueURL;
157   var UNICODEvsSYMBOL = top.UNICODEvsSYMBOL;
158   var mode_list = mode.split(",");
159   
160   var keys = "";
161   var url = "";
162
163   var interfaceURL = top.topurl + "/html/cic/index.html";
164   var thinterfaceURL = top.topurl + "/html/theory/index.html";
165
166   var output = mode_list[0];
167   var format;
168   if (output == "raw") format = mode_list[1];
169   else format = mode_list[2];
170   
171   if (output == "raw") {
172     var ext = "";
173     var rdfprefix = "";
174     if (format == "types") ext = ".types"
175     else if (format == "ann") ext = ".ann"
176     else if (format == "fwd") rdfprefix = "helm:rdf:www.cs.unibo.it/helm/rdf/forward//"
177     else if (format == "bwd") rdfprefix = "helm:rdf:www.cs.unibo.it/helm/rdf/backward//";
178     url = getterURL + "getxml?uri=" + rdfprefix + uri + ext + "&format=" +
179           mode_list[5] + "&patch_dtd=" + mode_list[6];
180   } else {
181     if (format == "html" && type == "cic") {
182       keys = getCICHTMLKeys() +
183        "&param.processorURL=" + escape(processorURL) +
184        "&param.getterURL=" + escape(getterURL) +
185        "&param.proofcheckerURL=" + escape(proofcheckerURL) +
186        "&param.draw_graphURL=" + escape(draw_graphURL) +
187        "&param.uri_set_queueURL=" + escape(uri_set_queueURL) +
188        "&param.UNICODEvsSYMBOL=" + escape(UNICODEvsSYMBOL) +
189        "&prop.doctype-public="+escape("-//W3C//DTD XHTML 1.0 Transitional//EN")+
190        "&prop.encoding=iso-8859-1" +
191        "&prop.media-type=text/html" +
192        "&param.doctype-public="+escape("-//W3C//DTD XHTML 1.0 Transitional//EN")+
193        "&param.encoding=iso-8859-1" +
194        "&param.media-type=text/html" +
195        "&param.keys=" + getCICHTMLKeys() +
196        "&param.interfaceURL=" + escape(interfaceURL);
197     } else if (format == "html" && type == "theory") {
198       keys = getTheoryKeys()+
199        "&param.processorURL=" + escape(processorURL) +
200        "&param.getterURL=" + escape(getterURL) +
201        "&param.proofcheckerURL=" + escape(proofcheckerURL) +
202        "&param.draw_graphURL=" + escape(draw_graphURL) +
203        "&param.uri_set_queueURL=" + escape(uri_set_queueURL) +
204        "&param.UNICODEvsSYMBOL=" + escape(UNICODEvsSYMBOL) +
205        "&param.keys=" + getCICHTMLKeys() +
206        "&param.thkeys=" + getTheoryKeys() +
207        "&param.embedkeys=" + getEmbedKeys() +
208        "&param.doctype-public="+escape("-//W3C//DTD XHTML 1.0 Transitional//EN")+
209        "&param.encoding=iso-8859-1" +
210        "&param.thencoding=iso-8859-1" +
211        "&param.media-type=text/html" +
212        "&param.thmedia-type=text/html" +
213        "&param.interfaceURL=" + escape(interfaceURL) +
214        "&param.thinterfaceURL=" + escape(thinterfaceURL);
215     } else if (format == "mml_cont" && type == "cic") {
216       keys = escape("d_c,C1")+
217        "&prop.doctype-public="+
218        "&prop.encoding=" +
219        "&prop.media-type=text/xml" +
220        "&param.doctype-public=" +
221        "&param.encoding=" +
222        "&param.media-type=text/xml";
223     } else if (format == "mml_cont" && type == "theory") {
224       keys = escape("T1,L,E")+
225        "&param.keys=" + escape("d_c,C1") +
226        "&param.thkeys=T1,L,E" +
227        "&param.embedkeys=" + escape("d_c,TC1") +
228
229        "&param.processorURL=" + escape(processorURL) +
230        "&param.getterURL=" + escape(getterURL) +
231        "&param.proofcheckerURL=" + escape(proofcheckerURL) +
232        "&param.draw_graphURL=" + escape(draw_graphURL) +
233        "&param.uri_set_queueURL=" + escape(uri_set_queueURL) +
234        "&param.doctype-public=" +
235        "&param.encoding=" +
236        "&param.thencoding=iso-8859-1" +
237        "&param.media-type=text/xml" +
238        "&param.thmedia-type=text/html" +
239        "&param.interfaceURL=" + escape(interfaceURL) +
240        "&param.thinterfaceURL=" + escape(thinterfaceURL);
241     } else if (format == "mml_pres" && type == "cic") {
242       keys = getCICMathMLKeys()+
243        "&param.processorURL=" + escape(processorURL) +
244        "&param.getterURL=" + escape(getterURL) +
245        "&param.proofcheckerURL=" + escape(proofcheckerURL) +
246        "&param.draw_graphURL=" + escape(draw_graphURL) +
247        "&param.uri_set_queueURL=" + escape(uri_set_queueURL) +
248        "&prop.doctype-public="+
249        "&prop.encoding=" +
250        "&prop.media-type=text/xml" +
251        "&param.doctype-public=" +
252        "&param.encoding=" +
253        "&param.media-type=text/xml" +
254        "&param.keys=" + getCICMathMLKeys() +
255        "&param.interfaceURL=" + escape(interfaceURL);
256     } else if (format == "mml_pres" && type == "theory") {
257       keys = getTheoryKeys()+
258        "&param.keys=" + getCICMathMLKeys() +
259        "&param.thkeys=" + getTheoryKeys() +
260        "&param.embedkeys=" + escape("d_c,TC1,G,C2,L") +
261        "&param.processorURL=" + escape(processorURL) +
262        "&param.getterURL=" + escape(getterURL) +
263        "&param.proofcheckerURL=" + escape(proofcheckerURL) +
264        "&param.draw_graphURL=" + escape(draw_graphURL) +
265        "&param.uri_set_queueURL=" + escape(uri_set_queueURL) +
266        "&param.doctype-public=" +
267        "&param.encoding=" +
268        "&param.thencoding=iso-8859-1" +
269        "&param.media-type=text/xml" +
270        "&param.thmedia-type=text/html" +
271        "&param.interfaceURL=" + escape(interfaceURL) +
272        "&param.thinterfaceURL=" + escape(thinterfaceURL);
273     }
274
275     var naturalLanguage = typesflags.toLowerCase();
276     if (typesflags != "NO" || type == "theory") {
277        naturalLanguage = mode_list[3];
278     }
279     var annotations = cicflags.toLowerCase();
280     if (cicflags != "NO" || type == "theory") {
281        annotations = mode_list[4];
282     }
283     url = processorURL + "apply?xmluri=" + escape(getterURL + "getxml?uri=" + uri) + "&keys=" + keys + "&param.CICURI=" + uri + "&param.naturalLanguage=" + naturalLanguage + "&param.annotations=" + annotations + "&param.topurl=" + top.topurl;
284   }
285
286   if (output == "raw")
287    return url;
288   else if (type == "cic")
289    return interfaceURL + "?url=" + escape(url);
290   else if (type == "theory")
291    return thinterfaceURL + "?url=" + escape(url)
292 }
293