<script language="javascript">
<!-- Start Hiding the Script
// Add an option to the list of options
function addOption(val,txt) {
pos = document.wr_plugins.options.length;
++document.wr_plugins.options.length;
document.wr_plugins.options[pos].value = val;
document.wr_plugins.options[pos].text = txt;
}// Make the browser open the given URL in the toplevel window, immediately.
function unravelPage(page) {
  document.location.href=page;
  return page;
}
// Handle a selected option.
function handleOption() {
if (document.wr_plugins.plugin.selectedIndex == 0) {
alert("You must select a plug-in first");
}
else {
ind = document.wr_plugins.options.selectedIndex;
cmd = document.wr_plugins.options[ind].value;
plugin = document.wr_plugins.plugin.value;
// URL form for activate/deactivate/disable
if ( (cmd == "activate") || (cmd == "deactivate") || (cmd == "disable") ) {
tmp = "http://temp.webraveler2.config.userconfig/" 
	+ plugin
	+ "_" + cmd + "/";
}
// Standard URL form
else
tmp = "http://perm.webraveler2.plugin/"
 	+ plugin + "/" + cmd + "/";
window.open(tmp,'mywindow','width=600,height=800');
}
}
// Set up the screen so that it's clear the plug-in is active.
function pluginActive() {
document.wr_plugins.activity.value = "Active";
document.wr_plugins.options[4].text = "Deactivate";
document.wr_plugins.options[4].value = "deactivate";
}
// Set up the screen so that it's clear the plug-in is inactive.
function pluginInactive() {
document.wr_plugins.activity.value = "Inactive";
document.wr_plugins.options[4].text = "Activate";
document.wr_plugins.options[4].value = "activate";
}
// Observe that a plug-in has been selected.    This requires us to
// update all sorts of stuff on the screen.  Note that this portion of
// the script must be generated dynamically, depending on the current
// list of plugins and status of those plugins.
function selectedPlugin() {
// Chop down the menu (useful for all plugins).
document.wr_plugins.options.length = 5;
// Determine the name of the plugin
plugin = document.wr_plugins.plugin.value;
if (plugin == "None") {
document.wr_plugins.status.value = "STATUS";}
