diff --git a/collects/scribblings/main/private/make-search.ss b/collects/scribblings/main/private/make-search.ss index 6bb1a2734d..8d31a48fc9 100644 --- a/collects/scribblings/main/private/make-search.ss +++ b/collects/scribblings/main/private/make-search.ss @@ -135,7 +135,7 @@ (add-between ms ",\n "))}; // Globally visible bindings - var key_handler, toggle_help_pref, hide_prefs, new_query, refine_query, + var key_handler, toggle_panel, hide_prefs, new_query, refine_query, set_show_manuals, set_show_manual_titles, set_results_num, set_type_delay, set_highlight_color; @@ -151,7 +151,7 @@ var background_color = "#f8f8f8"; var query, status, results_container, result_links, - prev_page_link, next_page_link, panel; + prev_page_link, next_page_link; // tabIndex fields are set: // 1 query @@ -169,24 +169,28 @@ +' bgcolor='+background_color+'>' +'' +'' + +' tabIndex="1" onkeydown="return key_handler(event);"' + +' onkeydown="return key_handler(null);" />' +'' - +'[?]' + +'[!]' +'' - +'' + +' background-color: #f0f0f0;">' +'
' + +' of changing it (some browsers don\'t support this)' + +'' + +'' + +'' +'Preferences:
' +'Show manuals:' +'