diff options
author | idontgetoutmuch <dominic@steinitz.org> | 2015-12-20 21:01:47 +0000 |
---|---|---|
committer | idontgetoutmuch <dominic@steinitz.org> | 2015-12-20 21:01:47 +0000 |
commit | 2bdfda1fb2e0de696ca8c6f7a152b2f85a541be9 (patch) | |
tree | cc29895f7d69f051cfec172bb0f8c2ef03552789 /haddock-api/resources/html/haddock-util.js | |
parent | 5a57a24c44e06e964c4ea2276c842c722c4e93d9 (diff) | |
parent | fa03f80d76f1511a811a0209ea7a6a8b6c58704f (diff) |
Merge pull request #1 from haskell/ghc-head
Ghc head
Diffstat (limited to 'haddock-api/resources/html/haddock-util.js')
-rw-r--r-- | haddock-api/resources/html/haddock-util.js | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/haddock-api/resources/html/haddock-util.js b/haddock-api/resources/html/haddock-util.js index 9a6fccf7..fc7743fe 100644 --- a/haddock-api/resources/html/haddock-util.js +++ b/haddock-api/resources/html/haddock-util.js @@ -131,11 +131,11 @@ 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)); @@ -166,7 +166,7 @@ function perform_search(full) status.innerHTML = ""; } - + function setclass(first, last, status) { for (var i = first; i <= last; i++) @@ -174,8 +174,8 @@ function perform_search(full) 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) @@ -201,9 +201,9 @@ function perform_search(full) 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) @@ -212,8 +212,8 @@ function perform_search(full) if (s == text) return 0; else return (s > text ? -1 : 1); } - - + + // from an index, get its string // this abstracts over alternates function getitem(i) @@ -229,7 +229,7 @@ function perform_search(full) } function setSynopsis(filename) { - if (parent.window.synopsis) { + if (parent.window.synopsis && parent.window.synopsis.location) { if (parent.window.synopsis.location.replace) { // In Firefox this avoids adding the change to the history. parent.window.synopsis.location.replace(filename); @@ -250,7 +250,7 @@ function addMenuItem(html) { 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>"); |