aboutsummaryrefslogtreecommitdiff
path: root/resources/html/haddock-util.js
diff options
context:
space:
mode:
Diffstat (limited to 'resources/html/haddock-util.js')
-rw-r--r--resources/html/haddock-util.js344
1 files changed, 0 insertions, 344 deletions
diff --git a/resources/html/haddock-util.js b/resources/html/haddock-util.js
deleted file mode 100644
index 9a6fccf7..00000000
--- a/resources/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 &#9662;</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();
-}
-