build style menu in javascript

	moved to javascript, so as to not polute the content with the style menu
	removed menu building code in Themes.hs
	removed onclick in Utils.hs
changed text of button in header from "Source code" to "Source"
	more consistent with links in rest of page

1 files changed, 42 insertions, 11 deletions

diff --git a/html/haddock-util.js b/html/haddock-util.js
index 1a57b24b..c5bc6a8d 100644
--- a/html/haddock-util.js
+++ b/html/haddock-util.js
@@ -164,23 +164,27 @@ function perform_search(full)
     }
 }
 
-function addFramesButton() {
-  if (parent.location.href == window.location.href) {
-    var menu = document.getElementById("page-menu");
-    if (menu) {
-      var btn = menu.lastChild.cloneNode(false);
-      btn.innerHTML = "<a href='#' onclick='reframe();return true;'>Frames</a>";
-      menu.appendChild(btn);
-    }
-  }
-}
-
 function setSynopsis(filename) {
     if (parent.window.synopsis) {
       parent.window.synopsis.location = filename;
     }
 }
 
+function addMenuItem(html) {
+  var menu = document.getElementById("page-menu");
+  if (menu) {
+    var btn = menu.firstChild.cloneNode(false);
+    btn.innerHTML = html;
+    menu.appendChild(btn);
+  }
+}
+
+function addFramesButton() {
+  if (parent.location.href == window.location.href) {
+    addMenuItem("<a href='#' onclick='reframe();return true;'>Frames</a>");
+  }
+}
+
 function reframe() {
   setCookie("haddock-reframe", document.URL);
   window.location = "frames.html";
@@ -194,6 +198,26 @@ function postReframe() {
   }
 }
 
+function addStyleMenu() {
+  var i, a, c = 0, btns = "";
+  for(i=0; (a = document.getElementsByTagName("link")[i]); i++) {
+    if(a.getAttribute("rel").indexOf("style") != -1
+       && a.getAttribute("title")) {
+      btns += "<li><a href='#' onclick=\"setActiveStyleSheet('"
+        + a.getAttribute("href") + "'); return false;\">"
+        + a.getAttribute("title") + "</a></li>"
+      c += 1;
+    }
+  }
+  if (c > 1) {
+    var h = "<div id='style-menu-holder'>"
+      + "<a href='#' onclick='styleMenu(); return false;'>Style &#9662;</a>"
+      + "<ul id='style-menu' class='hide'>" + btns + "</ul>"
+      + "</div>";
+    addMenuItem(h);
+  }
+}
+
 function setActiveStyleSheet(href) {
   var i, a, found = false;
   for(i=0; (a = document.getElementsByTagName("link")[i]); i++) {
@@ -223,3 +247,10 @@ function styleMenu(show) {
   toggleClassShow(m, show);
 }
 
+
+function pageLoad() {
+  addStyleMenu();
+  addFramesButton();
+  resetStyle();
+}
+