]> matita.cs.unibo.it Git - helm.git/blob - helm/on-line/javascript/control.js
top.topurl alias topurl alias interfaceURL alias thinterfaceURL is no
[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 mode_list = mode.split(",");
26   var new_mode = output.options[output.selectedIndex].value;
27   var dest = "?theoryuri=" + theoryuri + "&cicuri=" + cicuri + "&topurl=" + topurl + "&processorURL=" + processorURL + "&getterURL=" + getterURL + "&mode=";
28   
29   if (new_mode != mode_list[0]) {
30     updateMode(0, new_mode);
31     if (new_mode == "raw") updateMode(2, format.options[format.selectedIndex].value);
32     else updateMode(1, format.options[format.selectedIndex].value);
33     location.search = dest + top.mode;
34   }
35 }
36
37 function updateFormat(format)
38 {
39   var mode = top.mode;
40   var mode_list = mode.split(",");
41
42   if (mode_list[0] == "raw") {
43     updateMode(1, format.options[format.selectedIndex].value);
44   } else {
45     updateMode(2, format.options[format.selectedIndex].value);
46   }
47
48   refreshReload();
49 }
50
51 function updateNatural(checkbox)
52 {
53   if (checkbox.checked) updateMode(3, "yes");
54   else updateMode(3, "no");
55   refreshReload();
56 }
57
58 function updateAnnotations(checkbox)
59 {
60   if (checkbox.checked) updateMode(4, "yes");
61   else updateMode(4, "no");
62   refreshReload();
63 }
64
65 function updateCompressed(checkbox)
66 {
67   if (checkbox.checked) updateMode(5, "gz");
68   else updateMode(5, "normal");
69   refreshReload();
70 }
71
72 function updateDTDPatched(checkbox)
73 {
74   if (checkbox.checked) updateMode(6, "yes");
75   else updateMode(6, "no");
76   refreshReload();
77 }
78
79 function refreshReload()
80 {
81    var search = 
82       "?mode=" + top.mode +
83       "&cicuri=" + top.cicuri +
84       "&theoryuri=" + top.theoryuri +
85       "&processorURL=" + top.processorURL +
86       "&getterURL=" + top.getterURL +
87       "&UNICODEvsSYMBOL=" + top.UNICODEvsSYMBOL;
88
89    top.frames[0].document.links[0].search = search;
90    top.frames[0].document.links[1].search = search;
91
92    return true;
93 }
94
95 function refreshcicHeader(headerURL)
96 {
97    top.cicheader.location.search = "?keys=GP&xmluri=" + headerURL + "&param.uri=" + top.cicuri;
98    return true;
99 }
100
101 function refreshtheoryHeader(headerURL)
102 {
103    top.theoryheader.location.search = "?keys=GP&xmluri=" + headerURL + "&param.uri=" + top.theoryuri;
104    return true;
105 }
106
107 function getCICMathMLKeys()
108 {
109   //Important note: do not modify this function without modifying makeURL
110   return escape("d_c,C1,G,C2,L");
111 }
112
113 function makeURL(type,uri,cicflags,typesflags)
114 {
115   var mode = top.mode;
116   var processorURL = top.processorURL;
117   var getterURL = top.getterURL;
118   var UNICODEvsSYMBOL = top.UNICODEvsSYMBOL;
119   var mode_list = mode.split(",");
120   
121   var keys = "";
122   var url = "";
123
124   var interfaceURL = top.topurl + "/html/cic/index.html";
125   var thinterfaceURL = top.topurl + "/html/theory/index.html";
126
127   var output = mode_list[0];
128   var format;
129   if (output == "raw") format = mode_list[1];
130   else format = mode_list[2];
131   
132   if (output == "raw") {
133     var ext = "";
134     if (format == "types") ext = ".types"
135     else if (format == "ann") ext = ".ann";
136     url = getterURL + "getxml?uri=" + uri + ext + "&format=" + mode_list[5] +
137      "&patch_dtd=" + mode_list[6];
138   } else {
139     if (format == "html" && type == "cic") {
140       //Important note: do not modify this function without modifying
141       //getCICMathMLKeys
142       keys = escape("d_c,C1,HC2,L")+"&param.processorURL=" + escape(processorURL) +
143        "&param.getterURL=" + escape(getterURL) +
144        "&param.UNICODEvsSYMBOL=" + escape(UNICODEvsSYMBOL) +
145        "&prop.doctype-public="+escape("-//W3C//DTD XHTML 1.0 Transitional//EN")+
146        "&prop.encoding=iso-8859-1" +
147        "&prop.media-type=text/html" +
148        "&param.doctype-public="+escape("-//W3C//DTD XHTML 1.0 Transitional//EN")+
149        "&param.encoding=iso-8859-1" +
150        "&param.media-type=text/html" +
151        "&param.keys=" + escape("C1,HC2,L") +
152        "&param.interfaceURL=" + escape(interfaceURL);
153     } else if (format == "html" && type == "theory") {
154       keys = escape("T1,T2,L,E")+
155        "&param.processorURL=" + escape(processorURL) +
156        "&param.getterURL=" + escape(getterURL) +
157        "&param.UNICODEvsSYMBOL=" + escape(UNICODEvsSYMBOL) +
158        "&param.keys=" + escape("C1,HC2,L") +
159        "&param.thkeys=" + escape("T1,T2,L,E") +
160        "&param.embedkeys=" + escape("TC1,HC2,L") +
161        "&param.doctype-public="+escape("-//W3C//DTD XHTML 1.0 Transitional//EN")+
162        "&param.encoding=iso-8859-1" +
163        "&param.thencoding=iso-8859-1" +
164        "&param.media-type=text/html" +
165        "&param.thmedia-type=text/html" +
166        "&param.interfaceURL=" + escape(interfaceURL) +
167        "&param.thinterfaceURL=" + escape(thinterfaceURL);
168     } else if (format == "mml_cont" && type == "cic") {
169       keys = "C1";
170     } else if (format == "mml_cont" && type == "theory") {
171       keys = escape("T1,L,E")+
172        "&param.keys=C1" +
173        "&param.thkeys=T1,L,E" +
174        "&param.embedkeys=TC1" +
175
176        "&param.processorURL=" + escape(processorURL) +
177        "&param.getterURL=" + escape(getterURL) +
178        "&param.doctype-public=" +
179        "&param.encoding=" +
180        "&param.thencoding=iso-8859-1" +
181        "&param.media-type=text/xml" +
182        "&param.thmedia-type=text/html" +
183        "&param.interfaceURL=" + escape(interfaceURL) +
184        "&param.thinterfaceURL=" + escape(thinterfaceURL);
185     } else if (format == "mml_pres" && type == "cic") {
186       keys = escape("C1,G,C2,L")+
187        "&param.processorURL=" + escape(processorURL) +
188        "&param.getterURL=" + escape(getterURL) +
189        "&prop.doctype-public="+
190        "&prop.encoding=" +
191        "&prop.media-type=text/xml" +
192        "&param.doctype-public=" +
193        "&param.encoding=" +
194        "&param.media-type=text/xml" +
195        "&param.keys=" + escape("C1,G,C2,L") +
196        "&param.interfaceURL=" + escape(interfaceURL);
197     } else if (format == "mml_pres" && type == "theory") {
198       keys = escape("T1,T2,L,E")+
199        "&param.keys=C1,G,C2,L" +
200        "&param.thkeys=T1,T2,L,E" +
201        "&param.embedkeys=TC1,G,C2,L" +
202        "&param.processorURL=" + escape(processorURL) +
203        "&param.getterURL=" + escape(getterURL) +
204        "&param.doctype-public=" +
205        "&param.encoding=" +
206        "&param.thencoding=iso-8859-1" +
207        "&param.media-type=text/xml" +
208        "&param.thmedia-type=text/html" +
209        "&param.interfaceURL=" + escape(interfaceURL) +
210        "&param.thinterfaceURL=" + escape(thinterfaceURL);
211     }
212
213     var naturalLanguage = typesflags;
214     if (typesflags != "NO" || type == "theory") {
215        naturalLanguage = mode_list[3];
216     }
217     var annotations = cicflags;
218     if (cicflags != "NO" || type == "theory") {
219        annotations = mode_list[4];
220     }
221     url = processorURL + "apply?xmluri=" + escape(getterURL + "getxml?uri=" + uri) + "&keys=" + keys + "&param.CICURI=" + uri + "&param.naturalLanguage=" + naturalLanguage + "&param.annotations=" + annotations;
222   }
223
224   if (output == "raw")
225    return url;
226   else if (type == "cic")
227    return interfaceURL + "?url=" + escape(url);
228   else if (type == "theory")
229    return thinterfaceURL + "?url=" + escape(url)
230 }
231