// Haddock JavaScript utilities function makeClassToggle(cOn, cOff) { var rOn = new RegExp('\\b'+cOn+'\\b'); var rOff = new RegExp('\\b'+cOff+'\\b'); return function(e, a) { var c = e.className; if (a == null) { a = rOff.test(c); } if (a) { c = c.replace(rOff, cOn); } else { c = c.replace(rOn, cOff); } e.className = c; } } toggleClassShow = makeClassToggle("show", "hide"); toggleClassCollapser = makeClassToggle("collapser", "expander"); function toggleSection(toggler,id) { toggleClassShow(document.getElementById(id)) toggleClassCollapser(toggler); } function setCookie(name, value) { document.cookie = name + "=" + escape(value) + ";path=/;"; } function clearCookie(name) { document.cookie = name + "=;path=/;expires=Thu, 01-Jan-1970 00:00:01 GMT;"; } function getCookie(name) { var nameEQ = name + "="; var ca = document.cookie.split(';'); for(var i=0;i < ca.length;i++) { var c = ca[i]; while (c.charAt(0)==' ') c = c.substring(1,c.length); if (c.indexOf(nameEQ) == 0) { return unescape(c.substring(nameEQ.length,c.length)); } } return null; } var max_results = 75; // 50 is not enough to search for map in the base libraries var shown_range = null; var last_search = null; function quick_search() { perform_search(false); } function full_search() { perform_search(true); } function perform_search(full) { var text = document.getElementById("searchbox").value.toLowerCase(); if (text == last_search && !full) return; last_search = text; var table = document.getElementById("indexlist"); var status = document.getElementById("searchmsg"); var children = table.firstChild.childNodes; // first figure out the first node with the prefix var first = bisect(-1); var last = (first == -1 ? -1 : bisect(1)); if (first == -1) { table.className = ""; status.innerHTML = "No results found, displaying all"; } else if (first == 0 && last == children.length - 1) { table.className = ""; status.innerHTML = ""; } else if (last - first >= max_results && !full) { table.className = ""; status.innerHTML = "More than " + max_results + ", press Search to display"; } else { // decide what you need to clear/show if (shown_range) setclass(shown_range[0], shown_range[1], "indexrow"); setclass(first, last, "indexshow"); shown_range = [first, last]; table.className = "indexsearch"; status.innerHTML = ""; } function setclass(first, last, status) { for (var i = first; i <= last; i++) { children[i].className = status; } } // do a binary search, treating 0 as ... // return either -1 (no 0's found) or location of most far match function bisect(dir) { var first = 0, finish = children.length - 1; var mid, success = false; while (finish - first > 3) { mid = Math.floor((finish + first) / 2); var i = checkitem(mid); if (i == 0) i = dir; if (i == -1) finish = mid; else first = mid; } var a = (dir == 1 ? first : finish); var b = (dir == 1 ? finish : first); for (var i = b; i != a - dir; i -= dir) { if (checkitem(i) == 0) return i; } return -1; } // from an index, decide what the result is // 0 = match, -1 is lower, 1 is higher function checkitem(i) { var s = getitem(i).toLowerCase().substr(0, text.length); if (s == text) return 0; else return (s > text ? -1 : 1); } // from an index, get its string // this abstracts over alternates function getitem(i) { for ( ; i >= 0; i--) { var s = children[i].firstChild.firstChild.data; if (s.indexOf(' ') == -1) return s; } return ""; // should never be reached } } 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("Frames"); } } function reframe() { setCookie("haddock-reframe", document.URL); window.location = "frames.html"; } function postReframe() { var s = getCookie("haddock-reframe"); if (s) { parent.window.main.location = s; clearCookie("haddock-reframe"); } } 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 += "