From 208e5e87a92f8d804c87f6812bebda2a97ff27b7 Mon Sep 17 00:00:00 2001
From: Neil Mitchell <http://www.cs.york.ac.uk/~ndm/>
Date: Fri, 12 Jan 2007 12:17:46 +0000
Subject: 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))

---
 html/haddock-util.js | 109 ++++++++++++++++++++++++++++++++++++++++++++++-----
 1 file changed, 100 insertions(+), 9 deletions(-)

(limited to 'html/haddock-util.js')

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
     }
 }
-- 
cgit v1.2.3