diff options
Diffstat (limited to 'html/haddock-util.js')
| -rw-r--r-- | html/haddock-util.js | 344 |
1 files changed, 0 insertions, 344 deletions
diff --git a/html/haddock-util.js b/html/haddock-util.js deleted file mode 100644 index 9a6fccf7..00000000 --- a/html/haddock-util.js +++ /dev/null @@ -1,344 +0,0 @@ -// Haddock JavaScript utilities - -var rspace = /\s\s+/g, - rtrim = /^\s+|\s+$/g; - -function spaced(s) { return (" " + s + " ").replace(rspace, " "); } -function trim(s) { return s.replace(rtrim, ""); } - -function hasClass(elem, value) { - var className = spaced(elem.className || ""); - return className.indexOf( " " + value + " " ) >= 0; -} - -function addClass(elem, value) { - var className = spaced(elem.className || ""); - if ( className.indexOf( " " + value + " " ) < 0 ) { - elem.className = trim(className + " " + value); - } -} - -function removeClass(elem, value) { - var className = spaced(elem.className || ""); - className = className.replace(" " + value + " ", " "); - elem.className = trim(className); -} - -function toggleClass(elem, valueOn, valueOff, bool) { - if (bool == null) { bool = ! hasClass(elem, valueOn); } - if (bool) { - removeClass(elem, valueOff); - addClass(elem, valueOn); - } - else { - removeClass(elem, valueOn); - addClass(elem, valueOff); - } - return bool; -} - - -function makeClassToggle(valueOn, valueOff) -{ - return function(elem, bool) { - return toggleClass(elem, valueOn, valueOff, bool); - } -} - -toggleShow = makeClassToggle("show", "hide"); -toggleCollapser = makeClassToggle("collapser", "expander"); - -function toggleSection(id) -{ - var b = toggleShow(document.getElementById("section." + id)); - toggleCollapser(document.getElementById("control." + id), b); - rememberCollapsed(id, b); - return b; -} - -var collapsed = {}; -function rememberCollapsed(id, b) -{ - if(b) - delete collapsed[id] - else - collapsed[id] = null; - - var sections = []; - for(var i in collapsed) - { - if(collapsed.hasOwnProperty(i)) - sections.push(i); - } - // cookie specific to this page; don't use setCookie which sets path=/ - document.cookie = "collapsed=" + escape(sections.join('+')); -} - -function restoreCollapsed() -{ - var cookie = getCookie("collapsed"); - if(!cookie) - return; - - var ids = cookie.split('+'); - for(var i in ids) - { - if(document.getElementById("section." + ids[i])) - toggleSection(ids[i]); - } -} - -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) { - if (parent.window.synopsis.location.replace) { - // In Firefox this avoids adding the change to the history. - parent.window.synopsis.location.replace(filename); - } else { - 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 adjustForFrames() { - var bodyCls; - - if (parent.location.href == window.location.href) { - // not in frames, so add Frames button - addMenuItem("<a href='#' onclick='reframe();return true;'>Frames</a>"); - bodyCls = "no-frame"; - } - else { - bodyCls = "in-frame"; - } - addClass(document.body, bodyCls); -} - -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 styles() { - var i, a, es = document.getElementsByTagName("link"), rs = []; - for (i = 0; a = es[i]; i++) { - if(a.rel.indexOf("style") != -1 && a.title) { - rs.push(a); - } - } - return rs; -} - -function addStyleMenu() { - var as = styles(); - var i, a, btns = ""; - for(i=0; a = as[i]; i++) { - btns += "<li><a href='#' onclick=\"setActiveStyleSheet('" - + a.title + "'); return false;\">" - + a.title + "</a></li>" - } - if (as.length > 1) { - var h = "<div id='style-menu-holder'>" - + "<a href='#' onclick='styleMenu(); return false;'>Style ▾</a>" - + "<ul id='style-menu' class='hide'>" + btns + "</ul>" - + "</div>"; - addMenuItem(h); - } -} - -function setActiveStyleSheet(title) { - var as = styles(); - var i, a, found; - for(i=0; a = as[i]; i++) { - a.disabled = true; - // need to do this always, some browsers are edge triggered - if(a.title == title) { - found = a; - } - } - if (found) { - found.disabled = false; - setCookie("haddock-style", title); - } - else { - as[0].disabled = false; - clearCookie("haddock-style"); - } - styleMenu(false); -} - -function resetStyle() { - var s = getCookie("haddock-style"); - if (s) setActiveStyleSheet(s); -} - - -function styleMenu(show) { - var m = document.getElementById('style-menu'); - if (m) toggleShow(m, show); -} - - -function pageLoad() { - addStyleMenu(); - adjustForFrames(); - resetStyle(); - restoreCollapsed(); -} - |