]> matita.cs.unibo.it Git - helm.git/blob - helm/on-line/html/library/control.html
72c13b65f63bc4ab03de914953b392b58e830eee
[helm.git] / helm / on-line / html / library / control.html
1 <?xml version="1.0" encoding="UTF-8"?>
2 <!--
3 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "DTD/xhtml1-strict.dtd">
4 -->
5
6 <html xmlns:subst="http://www.cs.unibo.it/helm/subst">
7 <head>
8 <title>Control panel</title>
9 <!-- Note: <subst:script/> are substitued by the stylesheet with <script />  -->
10 <!-- after changing @src in the concatenation of the interface URL with @src -->
11 <subst:script language="JavaScript" src="/javascript/defaults.js" />
12 <subst:script language="JavaScript" src="/javascript/utils.js" />
13 <subst:script language="JavaScript" src="/javascript/control.js" />
14 </head>
15 <body bgcolor="#ffffff" text="#000000">
16 <form>
17 <table>
18   <tr>
19     <td>
20       <b>Format</b>:
21     </td>
22     <td>
23       <select name="output" onChange="updateOutput(this,document.forms[0].format)">
24       <script>
25         var mode = getParam2('mode');
26         var mode_list = mode.split(',');
27         outputOption(document, "processed", "Processed", mode_list[0]);
28         outputOption(document, "raw", "Raw", mode_list[0]);
29       </script>
30       </select>
31     </td>
32     <td>
33       <select name="format" onChange="updateFormat(this)">
34       <script>
35         var mode = getParam2('mode');
36         var mode_list = mode.split(',');
37         if (mode_list[0] == "raw") {
38           outputOption(document, "cic",   "CIC", mode_list[1]);
39           outputOption(document, "types", "TYPES", mode_list[1]);
40           outputOption(document, "ann",   "ANN", mode_list[1]);
41           outputOption(document, "fwd",   "RDF: Forward pointers", mode_list[1]);
42           outputOption(document, "bwd",   "RDF: Backward pointers", mode_list[1]);
43         } else {
44           outputOption(document, "html", "HTML", mode_list[2]);
45           outputOption(document, "mml_cont", "MathML Content", mode_list[2]);
46           outputOption(document, "mml_pres", "MathML Presentation", mode_list[2]);
47         }
48       </script>
49       </select>
50     </td>
51     <td>
52      <script>
53 <![CDATA[
54        document.write('<a target="_top" href="' +
55          getParam2('topurl') + '/html/library/index.html' +
56          '" onClick="refreshReload()">Reload</a>');
57 ]]>
58      </script>
59      <br />
60      (do it also before attempting to take a link to the current page)
61      <script>
62 <![CDATA[
63        top.processorURL = getParam2('processorURL');
64        top.getterURL = getParam2('getterURL');
65        top.proofcheckerURL = getParam2('proofcheckerURL');
66        top.draw_graphURL = getParam2('draw_graphURL');
67        top.uri_set_queueURL = getParam2('uri_set_queueURL');
68        top.UNICODEvsSYMBOL = getParam2('UNICODEvsSYMBOL');
69        top.topurl = getParam2('topurl');
70        top.mode = getParam2('mode');
71        top.cicuri = getParam2('cicuri');
72        top.theoryuri = getParam2('theoryuri');
73 ]]>
74      </script>
75     </td>
76   </tr>
77   <tr>
78     <td colspan="3">
79       <script>
80 <![CDATA[
81         var mode = getParam2('mode');
82         var mode_list = mode.split(',');
83         if (mode_list[0] == "raw") {
84          outputCheckbox(document, "updateCompressed(this)",
85           "&nbsp;Compressed", mode_list[5] == "gz");
86          outputCheckbox(document, "updateDTDPatched(this)",
87           "&nbsp;Resolve DTD URL", mode_list[6] == "yes");
88         } else {
89          outputCheckbox(document, "updateNatural(this)",
90           "&nbsp;Natural Language", mode_list[3] == "yes");
91          outputCheckbox(document, "updateAnnotations(this)",
92           "&nbsp;Annotations", mode_list[4] == "yes");
93         }
94 ]]>
95       </script>
96     </td>
97     <td>
98      <script>
99 <![CDATA[
100        document.write('<a target="_top" href=""' +
101          ' onClick="refreshReload()">Configuration Panel</a>');
102 ]]>
103      </script>
104      <br />
105     </td>
106   </tr>
107 </table>
108 </form>
109 </body>
110 </html>