Add searching on the index page

1 files changed, 27 insertions, 0 deletions

diff --git a/html/haddock-util.js b/html/haddock-util.js
index 4280d19c..fe471453 100644
--- a/html/haddock-util.js
+++ b/html/haddock-util.js
@@ -13,3 +13,30 @@ function toggle(button,id)
 	n.display = "none";
    }
 }
+
+
+function quick_search()
+{
+    perform_search(false);
+}
+
+function full_search()
+{
+    perform_search(true);
+}
+
+
+function perform_search(full)
+{
+    var text = document.getElementById("searchbox").value.toLowerCase();
+    var table = document.getElementById("indexlist");
+    var children = table.firstChild.childNodes;
+    for (var i = 0; i < children.length; i++)
+    {
+    	var c = children[i];
+    	var s = c.firstChild.firstChild.data;
+    	var show = s.toLowerCase().indexOf(text) != -1;
+    
+    	c.style.display = (show ? "" : "none");
+    }
+}