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