]> matita.cs.unibo.it Git - helm.git/commitdiff
getter's panel check in
authorStefano Zacchiroli <zack@upsilon.cc>
Mon, 7 Apr 2003 16:26:03 +0000 (16:26 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Mon, 7 Apr 2003 16:26:03 +0000 (16:26 +0000)
helm/http_getter/panel/.cvsignore [new file with mode: 0644]
helm/http_getter/panel/Makefile [new file with mode: 0644]
helm/http_getter/panel/control.html [new file with mode: 0644]
helm/http_getter/panel/control.js [new file with mode: 0644]
helm/http_getter/panel/index.html [new file with mode: 0644]
helm/http_getter/panel/welcome.html [new file with mode: 0644]

diff --git a/helm/http_getter/panel/.cvsignore b/helm/http_getter/panel/.cvsignore
new file mode 100644 (file)
index 0000000..5c9fd16
--- /dev/null
@@ -0,0 +1 @@
+getter-panel.tar.gz
diff --git a/helm/http_getter/panel/Makefile b/helm/http_getter/panel/Makefile
new file mode 100644 (file)
index 0000000..2663e20
--- /dev/null
@@ -0,0 +1,12 @@
+
+all:
+
+clean:
+       rm -f getter-panel.tar.gz
+
+cleanbak:
+       rm -rf *~
+
+dist: clean cleanbak
+       cd ..; tar cvfz getter-panel.tar.gz panel ; mv getter-panel.tar.gz panel
+
diff --git a/helm/http_getter/panel/control.html b/helm/http_getter/panel/control.html
new file mode 100644 (file)
index 0000000..60c60eb
--- /dev/null
@@ -0,0 +1,121 @@
+<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>
+
diff --git a/helm/http_getter/panel/control.js b/helm/http_getter/panel/control.js
new file mode 100644 (file)
index 0000000..45736aa
--- /dev/null
@@ -0,0 +1,35 @@
+
+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;
+  }
+}
+
diff --git a/helm/http_getter/panel/index.html b/helm/http_getter/panel/index.html
new file mode 100644 (file)
index 0000000..caeebcf
--- /dev/null
@@ -0,0 +1,8 @@
+<html>
+
+<frameset rows="75%,*">
+  <frame src="control.html" name="control"/>
+  <frame src="welcome.html" name="result"/>
+</frameset>
+
+</html>
diff --git a/helm/http_getter/panel/welcome.html b/helm/http_getter/panel/welcome.html
new file mode 100644 (file)
index 0000000..f6fbed4
--- /dev/null
@@ -0,0 +1,6 @@
+<html>
+
+<body bgcolor="white">
+</body>
+
+</html>