From a5049573a3fd9ffcc005262320baa981ce0b751d Mon Sep 17 00:00:00 2001 From: Eli Barzilay Date: Sun, 1 Jun 2008 02:05:07 +0000 Subject: [PATCH] added type delay to prefs svn: r10073 --- .../scribblings/main/private/make-search.ss | 28 +++++++++++++++---- 1 file changed, 22 insertions(+), 6 deletions(-) diff --git a/collects/scribblings/main/private/make-search.ss b/collects/scribblings/main/private/make-search.ss index 325bcd3750..081f7ac23c 100644 --- a/collects/scribblings/main/private/make-search.ss +++ b/collects/scribblings/main/private/make-search.ss @@ -123,13 +123,14 @@ // Globally visible bindings var key_handler, toggle_help_pref, hide_prefs, - set_results_num, set_highlight_color; + set_results_num, set_type_delay, set_highlight_color; (function(){ - // Configuration options - var results_num = (GetCookie("PLT_ResultsNum", false) || 20); - var highlight_color = (GetCookie("PLT_HighlightColor", false) || "#ffd"); + // Configuration options (use || in case the cookie exists but empty) + var results_num = (GetCookie("PLT_ResultsNum", false) || 20); + var type_delay = (GetCookie("PLT_TypeDelay", false) || 300) + var highlight_color = (GetCookie("PLT_HighlightColor", false) || "#ffd"); var background_color = "#f8f8f8"; var query, status, results_container, result_links, @@ -165,6 +166,10 @@ +'
' + +'Type delay:' + +'
' +'Exact matches color:' +'