aboutsummaryrefslogtreecommitdiff
path: root/haddock-api/resources/html
diff options
context:
space:
mode:
Diffstat (limited to 'haddock-api/resources/html')
-rw-r--r--haddock-api/resources/html/highlight.js46
1 files changed, 46 insertions, 0 deletions
diff --git a/haddock-api/resources/html/highlight.js b/haddock-api/resources/html/highlight.js
new file mode 100644
index 00000000..639cf5d5
--- /dev/null
+++ b/haddock-api/resources/html/highlight.js
@@ -0,0 +1,46 @@
+
+var styleForRule = function (rule) {
+ var sheets = document.styleSheets;
+ for (var s = 0; s < sheets.length; s++) {
+ var rules = sheets[s].cssRules;
+ for (var r = 0; r < rules.length; r++) {
+ if (rules[r].selectorText == rule) {
+ return rules[r].style;
+ }
+ }
+ }
+};
+
+var highlight = function () {
+ var color = styleForRule("a:hover")["background-color"];
+ var links = document.getElementsByTagName('a');
+ for (var i = 0; i < links.length; i++) {
+ var that = links[i];
+ if (this.href == that.href) {
+ that.style["background-color"] = color;
+ }
+ }
+};
+
+/*
+ * I have no idea what is the proper antonym for "highlight" in this
+ * context. "Diminish"? "Unhighlight"? "Lowlight" sounds ridiculously
+ * so I like it.
+ */
+var lowlight = function () {
+ var links = document.getElementsByTagName('a');
+ for (var i = 0; i < links.length; i++) {
+ var that = links[i];
+ if (this.href == that.href) {
+ that.style["background-color"] = "";
+ }
+ }
+};
+
+window.onload = function () {
+ var links = document.getElementsByTagName('a');
+ for (var i = 0; i < links.length; i++) {
+ links[i].onmouseover = highlight;
+ links[i].onmouseout = lowlight;
+ }
+};