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.childNodes[0].data = "-";
	n.display = "inline";
   } else {
	button.childNodes[0].data = "+";
	n.display = "none";
   }
}