diff --git a/collects/scribblings/main/private/make-search.ss b/collects/scribblings/main/private/make-search.ss index 0622a3e5f6..6bb1a2734d 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, + var key_handler, toggle_help_pref, hide_prefs, new_query, refine_query, set_show_manuals, set_show_manual_titles, set_results_num, set_type_delay, set_highlight_color; @@ -201,6 +201,8 @@ +' “L:”), other entries have a similar' +' manual links (using “T:”); you can' +' control whether manual links appear (and how) below' + +'
  • Right-clicking these links refines the current query instead' + +' of changing it
  • ' +'
    ' +'Preferences:
    ' +'Show manuals:' @@ -416,7 +418,8 @@ + '' + +' onclick="return new_query(this);"' + +' oncontextmenu="return refine_query(this);">' + desc[j] + ''; } else if (desc == "module") { note = 'module'; @@ -428,7 +431,8 @@ note += 'in ' + '' + +' onclick="return new_query(this);"' + +' oncontextmenu="return refine_query(this);">' + ((typeof idx == "number") ? (''+UncompactHtml(plt_search_data[idx][2])+'') : manual) @@ -529,6 +533,23 @@ } new_query = NewQuery; + // and this appends the the query to the current value (it's hooked + // on the oncontextmenu handler that doesn't work everywhere, but at + // least in FF and IE) + function RefineQuery(node) { + var m = node.href.search(/[?]q=[^?&@";"]+$/); + if (m < 0) return true; + m = decodeURIComponent(node.href.substring(m+3)); + if (query.value.indexOf(m) >= 0) return true; + else { + query.value = m + " " + query.value; + query.focus(); + DoSearch(); + return false; + } + } + refine_query = RefineQuery; + var panel_shown = false; function TogglePanel() { panel_shown = !panel_shown;