html/haddock.js


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

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