--- /dev/null
+<html>
+
+<head>
+<title>Getter Control Panel</title>
+
+<style type="text/css">
+#normal { background-color: white; font-family: sans-serif }
+td.head { font-weight: bold; background-color: #e6e6fa; color: brown }
+td.back { background-color: #e6e6fa; color: brown }
+#indent { margin-left: 1cm; margin-right: 1cm }
+</style>
+
+<script language="JavaScript" src="control.js">
+</script>
+
+</head>
+
+<body id="normal">
+<a name="top"/>
+<table border="0" width="100%" cellpadding="4">
+<tr><td class="head" align="center"><big><big>Getter Control Panel</big></big></td></tr>
+</table>
+
+<br />
+
+<div id="indent">
+This is a control panel for the HTTP getter. You can control a local or remote getter by filling
+the appropriate field below and sending the desired commands. In most cases, results of commands, such as error
+messages or documents, will be opened in the frame at the bottom of this page.
+Note that in order to use this page <i>you must have JavaScript enabled</i>.
+If you have troubles, please send an email to the author:
+<a href="mailto:luca.padovani@cs.unibo.it">luca.padovani@cs.unibo.it</a>
+</div>
+
+<div id="indent">
+<br />
+<table border="1">
+ <tr>
+ <td>
+ <form name="getterURL">
+ Getter <b>URL</b>
+ <script>
+ document.write('<input type="text" value="' + getInitialGetterURL() + '" size="50"/>');
+ </script>
+ <select onChange="selectGetterURL(this)">
+ <option value="">---</option>
+ <option value="localhost:8081/">localhost</option>
+ <option value="marcello.cs.unibo.it:8081/">marcello</option>
+ <option value="phd.cs.unibo.it:8081/">phd</option>
+ <option value="eolo.cs.unibo.it:8081/">eolo</option>
+ <option value="mowgli.cs.unibo.it:58081/">mowgli</option>
+ </select>
+ </form>
+ </td>
+ </tr>
+ <tr>
+ <td>
+ <form>
+ <b>Check</b> if Getter is running and request <b>Help</b>:<br />
+ <input type="button" value="Check & Help" onClick="top.result.location.replace(getGetterURL() + 'help')"/>
+ </form>
+ </td>
+ </tr>
+ <tr>
+ <td>
+ <form>
+ <b>Update</b> Getter's maps:<br />
+ <input type="button" value="Update" onClick="top.result.location.replace(getGetterURL() + 'update')"/>
+ </form>
+ </td>
+ </tr>
+ <tr>
+ <td>
+ <form>
+ <b>List</b> servers:<br />
+ <input type="button" value="List servers" onClick="top.result.location.replace(getGetterURL() + 'list_servers')"/>
+ </form>
+ </td>
+ </tr>
+ <tr>
+ <td>
+ <form name="addServer">
+ <b>Add</b> a server to the servers list:<br />
+ Server URL: <input type="text" name="url" size="50" value="http://" /><br />
+ Server position: <input type="text" name="position" value="0" /><br />
+ <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))"/>
+ </form>
+ </td>
+ </tr>
+ <tr>
+ <td>
+ <form name="removeServer">
+ <b>Remove</b> a server from the servers list:<br />
+ Server number: <input type="text" name="position" value="0" /><br />
+ <input type="button" value="Remove server" onClick="top.result.location.replace(getGetterURL() + 'remove_server?position=' + escape(document.removeServer.elements[0].value))"/>
+ </form>
+ </td>
+ </tr>
+</table>
+</div>
+
+<div id="indent">
+
+<table border="0">
+</table>
+
+</div>
+
+<div id="indent">
+ <br />
+ In case you want to customize the panel for your own needs, you can download
+ the source archive (HTML + JavaScript):
+ <ul>
+ <li>Getter Panel [<a href="getter-panel.tar.gz">.tar.gz</a>]</li>
+ </ul>
+</div>
+
+</body>
+
+</html>
+
--- /dev/null
+
+function getParam(name, def)
+{
+ var search = top.location.search;
+ search = search.slice(1);
+ var args = search.split("&");
+ var value = "-1";
+ for (var i = 0 ; i < args.length ; i++) {
+ var couple = args[i].split("=");
+ if (couple[0] == name) value = couple[1];
+ }
+ if (value == "-1") value = def;
+ return value;
+}
+
+function getInitialGetterURL()
+{
+ return getParam("getterURL", "http://mowgli.cs.unibo.it:58081/");
+}
+
+function getGetterURL()
+{
+ return document.getterURL.elements[0].value;
+}
+
+function selectGetterURL(ss)
+{
+ if (ss.selectedIndex == 0) {
+ document.getterURL.elements[0].value = "";
+ } else {
+ //document.getterURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":8081/";
+ document.getterURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value;
+ }
+}
+