]> matita.cs.unibo.it Git - helm.git/blob - helm/http_getter/panel/control.html
All the equalityTactics have now been ported to use both the equality of
[helm.git] / helm / http_getter / panel / control.html
1 <html>
2
3 <head>
4 <title>Getter Control Panel</title>
5
6 <style type="text/css">
7 #normal { background-color: white; font-family: sans-serif }
8 td.head { font-weight: bold; background-color: #e6e6fa; color: brown }
9 td.back { background-color: #e6e6fa; color: brown }
10 #indent { margin-left: 1cm; margin-right: 1cm }
11 </style>
12
13 <script language="JavaScript" src="control.js">
14 </script>
15
16 </head>
17
18 <body id="normal">
19 <a name="top"/>
20 <table border="0" width="100%" cellpadding="4">
21 <tr><td class="head" align="center"><big><big>Getter Control Panel</big></big></td></tr>
22 </table>
23
24 <br />
25
26 <div id="indent">
27 This is a control panel for the HTTP getter. You can control a local or remote getter by filling
28 the appropriate field below and sending the desired commands. In most cases, results of commands, such as error
29 messages or documents, will be opened in the frame at the bottom of this page.
30 Note that in order to use this page <i>you must have JavaScript enabled</i>.
31 If you have troubles, please send an email to the author:
32 <a href="mailto:luca.padovani@cs.unibo.it">luca.padovani@cs.unibo.it</a>
33 </div>
34
35 <div id="indent">
36 <br />
37 <table border="1">
38   <tr>
39     <td>
40       <form name="getterURL">
41         Getter <b>URL</b>
42         <script>
43           document.write('<input type="text" value="' + getInitialGetterURL() + '" size="50"/>');
44         </script>
45         <select onChange="selectGetterURL(this)">
46           <option value="">---</option>
47           <option value="localhost:8081/">localhost</option>
48           <option value="marcello.cs.unibo.it:8081/">marcello</option>
49           <option value="phd.cs.unibo.it:8081/">phd</option>
50           <option value="eolo.cs.unibo.it:8081/">eolo</option>
51           <option value="mowgli.cs.unibo.it:58081/">mowgli</option>
52         </select>
53       </form>
54     </td>
55   </tr>
56   <tr>
57     <td>
58       <form>
59         <b>Check</b> if Getter is running and request <b>Help</b>:<br />
60         <input type="button" value="Check & Help" onClick="top.result.location.replace(getGetterURL() + 'help')"/>
61       </form>
62     </td>
63   </tr>
64   <tr>
65     <td>
66       <form>
67         <b>Update</b> Getter's maps:<br />
68         <input type="button" value="Update" onClick="top.result.location.replace(getGetterURL() + 'update')"/>
69       </form>
70     </td>
71   </tr>
72   <tr>
73     <td>
74       <form>
75         <b>Clean cache</b> (must be done every time a file is modified)<br />
76         <input type="button" value="Clean" onClick="top.result.location.replace(getGetterURL() + 'clean_cache')"/>
77       </form>
78     </td>
79   </tr>
80   <tr>
81     <td>
82       <form>
83         <b>List</b> servers:<br />
84         <input type="button" value="List servers" onClick="top.result.location.replace(getGetterURL() + 'list_servers')"/>
85       </form>
86     </td>
87   </tr>
88   <tr>
89     <td>
90       <form name="addServer">
91         <b>Add</b> a server to the servers list:<br />
92         Server URL: <input type="text" name="url" size="50" value="http://" /><br />
93         Server position: <input type="text" name="position" value="0" /><br />
94         <input type="button" value="Add server" onClick="top.result.location.replace(getGetterURL() + 'add_server?url=' + escape(document.addServer.elements[0].value) +'&position=' + escape(document.addServer.elements[1].value))"/>
95       </form>
96     </td>
97   </tr>
98   <tr>
99     <td>
100       <form name="removeServer">
101         <b>Remove</b> a server from the servers list:<br />
102         Server number: <input type="text" name="position" value="0" /><br />
103         <input type="button" value="Remove server" onClick="top.result.location.replace(getGetterURL() + 'remove_server?position=' + escape(document.removeServer.elements[0].value))"/>
104       </form>
105     </td>
106   </tr>
107 </table>
108 </div>
109
110 <div id="indent">
111
112 <table border="0">
113 </table>
114
115 </div>
116
117 <div id="indent">
118   <br />
119   In case you want to customize the panel for your own needs, you can download
120   the source archive (HTML + JavaScript):
121   <ul>
122     <li>Getter Panel [<a href="getter-panel.tar.gz">.tar.gz</a>]</li>
123   </ul>
124 </div>
125
126 </body>
127
128 </html>
129