1 files changed, 100 insertions, 9 deletions

diff --git a/html/haddock-util.js b/html/haddock-util.js
index fe471453..ddc7f6d0 100644
--- a/html/haddock-util.js
+++ b/html/haddock-util.js
@@ -4,17 +4,21 @@ function toggle(button,id)
    var n = document.getElementById(id).style;
    if (n.display == "none")
    {
-	button.src = "minus.gif";
-	n.display = "block";
+    button.src = "minus.gif";
+    n.display = "block";
    }
    else
    {
-	button.src = "plus.gif";
-	n.display = "none";
+    button.src = "plus.gif";
+    n.display = "none";
    }
 }
 
 
+var max_results = 50;
+var shown_range = null;
+var last_search = null;
+
 function quick_search()
 {
     perform_search(false);
@@ -29,14 +33,101 @@ function full_search()
 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;
-    for (var i = 0; i < children.length; i++)
+    
+    // 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)
     {
-    	var c = children[i];
-    	var s = c.firstChild.firstChild.data;
-    	var show = s.toLowerCase().indexOf(text) != -1;
+        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;
+    }    
     
-    	c.style.display = (show ? "" : "none");
+    
+    // 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
     }
 }