diff options
Diffstat (limited to 'html')
-rw-r--r-- | html/haddock.css | 2 | ||||
-rw-r--r-- | html/haddock.js | 11 |
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"; + } +} |