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>"); | 
