diff --git a/collects/scribble/html-render.ss b/collects/scribble/html-render.ss index 18ae427315..4808c40142 100644 --- a/collects/scribble/html-render.ss +++ b/collects/scribble/html-render.ss @@ -186,17 +186,16 @@ [onchange "delayed_search(this.value,event);"] [onkeyup "delayed_search(this.value,event);"]))}) -(define (search-index-box index-url) ; appears on every page +) + +(define (search-index-box) ; appears on every page (let ([sa string-append]) `(input ([style ,(sa "font-size: 75%; margin: 0px; padding: 0px; border: 1px;" " background-color: #eee; color: #888;")] [type "text"] [value "...search..."] - [onkeypress ,(sa "if (event && event.keyCode==13" - " && this.value.indexOf(\"...search...\")<0) {" - " location=\"doc-index.html?q=\"+escape(this.value);" - " };")] + [onkeypress ,(format "return DoSearchKey(event, this, ~s);" (version))] [onfocus ,(sa "this.style.color=\"black\";" " if (this.value.indexOf(\"...search...\")>=0)" " this.value=\"\";")] @@ -204,8 +203,6 @@ " this.style.color=\"#888\";" " this.value=\"...search...\"; }")])))) -) - ;; ---------------------------------------- ;; main mixin @@ -611,9 +608,9 @@ #; ; no need for these index-local searches ,@(if (eq? d index) null - `((small nbsp - ,(search-index-box (derive-filename index)))))) - null)) + `((small nbsp ,(search-index-box))))) + null) + ,@(if up-path `(nbsp (small ,(search-index-box))) null)) (div ([class "navright"]) ,@(render (make-element diff --git a/collects/scribble/scribble-common.js b/collects/scribble/scribble-common.js index 1aef1c0db9..859654a69c 100644 --- a/collects/scribble/scribble-common.js +++ b/collects/scribble/scribble-common.js @@ -44,14 +44,15 @@ function NormalizePath(path) { return path; } -function DoSearchKey(event, field) { +function DoSearchKey(event, field, ver) { var val = field.value; if (event && event.keyCode == 13 && val.indexOf("...search...") < 0) { - var u = GetCookie("PLT_Root"); + var u = GetCookie("PLT_Root."+ver); if (u == null) u = "../"; // default: go up - u = u.replace(/[^\/\\]*$/, "") + "plt-search.html"; - location = u + "?q=" + escape(val); + location = u + "search/index.html" + "?q=" + escape(val); + return false; } + return true; } // `noscript' is problematic in some browsers (always renders as a diff --git a/collects/scribblings/main/private/make-search.ss b/collects/scribblings/main/private/make-search.ss index 60ea334127..460af938a3 100644 --- a/collects/scribblings/main/private/make-search.ss +++ b/collects/scribblings/main/private/make-search.ss @@ -137,7 +137,7 @@ @l]; // Globally visible bindings - var search_handler, page_up_handler, page_dn_handler; + var key_handler; (function(){ @@ -154,12 +154,12 @@ +'' +'' +'' +'
' +'' + +'onchange="key_handler(event);"' + +'onkeypress="return key_handler(event);" />' +'
' +'<<' +'' +'' @@ -167,7 +167,7 @@ +'' +'' +'>>' +'
' @@ -215,13 +215,15 @@ } } - var last_search_terms; + var last_search_term_raw, last_search_terms; var search_results, first_search_result; function DoSearch() { - var terms = - query.value.toLowerCase() - .replace(/\s\s*/g," ") // single spaces - .replace(/^\s/g,"").replace(/\s$/g,""); // trim edge spaces + var terms = query.value; + if (terms == last_search_term_raw) return; + last_search_term_raw = terms; + terms= terms.toLowerCase() + .replace(/\s\s*/g," ") // single spaces + .replace(/^\s/g,"").replace(/\s$/g,""); // trim edge spaces if (terms == last_search_terms) return; last_search_terms = terms; status.nodeValue = "Searching " + plt_search_data.length + " entries"; @@ -248,17 +250,6 @@ UpdateResults(); } - function PageDn() { - if (first_search_result + results_num < search_results.length) { - first_search_result += results_num; - UpdateResults(); - } - } - function PageUp() { - first_search_result -= results_num; - UpdateResults(); - } - function UncompactUrl(url) { return url.replace(/^>/, plt_main_url); } @@ -320,23 +311,34 @@ } var search_timer = null; - function DelayedSearch(event) { + function HandleKeyEvent(event) { if (search_timer != null) { var t = search_timer; search_timer = null; clearTimeout(t); } var key = event && event.keyCode; - if (key == 13) { DoSearch()@";" return false@";" } - else if (key == 33) { PageUp()@";" return false@";" } - else if (key == 34) { PageDn()@";" return false@";" } - else search_timer = setTimeout(DoSearch, 400); + if (key == 13) { + DoSearch(); + return false; + } else if (key == 33) { + DoSearch(); // in case we didn't update it yet + first_search_result -= results_num; + UpdateResults(); + return false; + } else if (key == 34) { + DoSearch(); // in case we didn't update it yet + if (first_search_result + results_num < search_results.length) { + first_search_result += results_num; + UpdateResults(); + } + return false; + } + search_timer = setTimeout(DoSearch, 400); return true; } - search_handler = DelayedSearch; - page_up_handler = PageUp; - page_dn_handler = PageDn; + key_handler = HandleKeyEvent; window.onload = InitializeSearch;