// Haddock JavaScript utilities
function toggle(id)
{
   var n = document.getElementById(id).style;
   if (n.display == "none")
   {
	n.display = "block";
   }
   else
   {
	n.display = "none";
   }
}