Rewrite much of the index searching code, previously was too slow to execute on the base library with IE, the new version guarantees less than O(log n) operations be performed, where n is the number in the list (before was always O(n))

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
     }
 }