html/haddock.js


1
2
3
4
5
6
7
8
9
10
11

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