2 files changed, 13 insertions, 0 deletions
diff --git a/html/haddock.css b/html/haddock.css
index 927d1ecd..b853bf76 100644
--- a/html/haddock.css
+++ b/html/haddock.css
@@ -35,6 +35,8 @@ TD.s15 {  height: 15px; }
 
 SPAN.keyword { text-decoration: underline; }
 
+BUTTON.coll { width : 2em; }
+
 /* --------- Documentation elements ---------- */
 
 TD.children {
diff --git a/html/haddock.js b/html/haddock.js
new file mode 100644
index 00000000..4f6a2e44
--- /dev/null
+++ b/html/haddock.js
@@ -0,0 +1,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";
+   }
+}