diff --git a/collects/scribblings/main/private/make-search.ss b/collects/scribblings/main/private/make-search.ss
index a6b729511f..fa9ea602da 100644
--- a/collects/scribblings/main/private/make-search.ss
+++ b/collects/scribblings/main/private/make-search.ss
@@ -178,13 +178,14 @@
(copy-file src dest)))
(define (make-search user-dir?)
- (make-paragraph
+ (make-splice
(list
- (script-ref "plt-index.js"
- #:noscript
- @list{Sorry, you must have JavaScript to use this page.})
- (script-ref "search.js")
- (make-render-element
- (make-with-attributes #f '((id . "plt_search_container")))
- null
- (lambda (r s i) (make-script user-dir? r s i))))))
+ (make-paragraph
+ (list
+ (script-ref "plt-index.js"
+ #:noscript
+ @list{Sorry, you must have JavaScript to use this page.})
+ (script-ref "search.js")
+ (make-render-element null null
+ (lambda (r s i) (make-script user-dir? r s i)))))
+ (make-styled-paragraph '() '(div-hack [id "plt_search_container"])))))
diff --git a/collects/scribblings/main/private/search.js b/collects/scribblings/main/private/search.js
index 4ccdc17e32..c6e7d6da00 100644
--- a/collects/scribblings/main/private/search.js
+++ b/collects/scribblings/main/private/search.js
@@ -1,12 +1,14 @@
// Globally visible bindings
var key_handler, toggle_panel, hide_prefs, new_query, refine_query,
- set_pre_query, set_show_manuals, set_show_manual_titles, set_results_num,
- set_type_delay, set_highlight_color, status_line, saved_status = false;
+ set_pre_query, set_context_query, set_show_manuals, set_show_manual_titles,
+ set_results_num, set_type_delay, set_highlight_color, status_line,
+ saved_status = false, pre_query_label_line;
(function(){
// Configuration options (use || in case a cookie exists but is empty)
var pre_query = GetCookie("PLT_PreQuery","");
+var pre_query_label = GetCookie("PLT_PreQueryLabel",""); // no prefs UI
var manual_settings = parseInt(GetCookie("PLT_ManualSettings",1));
var show_manuals = manual_settings % 10;
var show_manual_titles = ((manual_settings - show_manuals) / 10) > 0;
@@ -15,13 +17,15 @@ var type_delay = (parseInt(GetCookie("PLT_TypeDelay",false)) || 150);
var highlight_color = (GetCookie("PLT_HighlightColor",false) || "#ffd");
var background_color = "#f8f8f8";
-var query, results_container, result_links, prev_page_link, next_page_link;
+var query, results_container, result_links;
+var prev_page_link1, prev_page_link2, next_page_link1, next_page_link2;
// tabIndex fields are set:
// 1 query
// 2 index links
// 3 help/pref toggle
// 4 pref widgets
+// 5 clear current pre-filter context
// -1 prev/next page (un-tab-able)
function MakePref(label, input) {
@@ -37,131 +41,181 @@ function PrefInputArgs(name, desc) {
+' onchange="set_'+name+'(this); return true;"'
+' onfocus="saved_status=status_line.innerHTML;'
+'status_line.innerHTML=descriptions[\''+name+'\'];"'
- +' onblur="status_line.innerHTML = saved_status || \'\';"';
+ +' onblur="status_line.innerHTML=(saved_status || \'\');"';
+}
+
+function MakeChevrons(num, middle) {
+ return '
'
+ +'
<< '
+ +'
>> '
+ +middle
+ +'
';
+}
+
+function MakePreQueryItem(qry, desc) {
+ return ''
+ + desc.replace(/{{/g, "").replace(/}}/g, " ")
+ + ' ';
+}
+
+function MakeIcon(label,title,action) {
+ return ''+label+' '
}
function InitializeSearch() {
var n;
- n = document.getElementById("plt_search_container").parentNode;
- // hack the table in
- n.innerHTML = ''
- +'';
+ n = document.getElementById("plt_search_container");
+ // hack the dom widgets in
+ var panelbgcolor = "background-color: #f0f0f0;"
+ var panelstyle =
+ 'style="display: none; border: 1px solid #222; border-top: 0px;'
+ +' font-family: arial, sans-serif; margin: 0em 0em 1em 0em;'
+ +' padding: 0.5em; '+panelbgcolor+'"';
+ n.innerHTML =
+ ''
+ +'
'
+ +'
'
+ +MakeIcon("[?]", "help", "toggle_panel(\'help\')")
+ +MakeIcon("[!]", "preferences", "toggle_panel(\'prefs\')")
+ +'
'
+ +'
'
+ +'
'
+ +'
'
+ +MakeIcon("✕", "close", "toggle_panel(false)")
+ +'
'
+ +'
'
+ +'
'
+ +'Hit PageUp /PageDown and'
+ +' C+Enter /S+C+Enter to scroll through the'
+ +' results. '
+ +'Use “M:str ” to match only'
+ +' identifiers from modules that (partially) match'
+ +' “str ”; “M: ” by'
+ +' itself will restrict results to bound names only. '
+ +'“L:str ” is similar to'
+ +' “M:str ”, but'
+ +' “str ” should match the module name'
+ +' exactly. '
+ +'“T:str ” restricts results to ones in'
+ +' the “str ” manual (naming the'
+ +' directory where the manual is found). '
+ +'Entries that correspond to bindings have module links that'
+ +' create a query restricted to bindings in that module (using'
+ +' “L: ”), other entries have similar links for'
+ +' restricting results to a specific manual (using'
+ +' “T: ”); you can control whether manual links'
+ +' appear (and how) in the preferences. '
+ +'Right-clicking these links refines the current query instead of'
+ +' changing it (but some browsers don\'t support this). '
+ +' '
+ +'
'
+ +'
'
+ +'
'
+ +'
'
+ +'Clicking the following links will set your pre-query context to a'
+ +' few common choices:'
+ +'
'
+ +MakePreQueryItem("M:", "Bindings")
+ +MakePreQueryItem("T:reference", "Reference manual")
+ +MakePreQueryItem("M:scheme", "{{scheme}} bindings")
+ +MakePreQueryItem("M:scheme/base", "{{scheme/base}} bindings")
+ +' '
+ +'
'
+ +MakeChevrons(1,
+ '
')
+ +'
'
+ +'
'
+ +MakeChevrons(2,
+ '
')
+ +'
';
// get the widgets we use
query = document.getElementById("search_box");
status_line = document.getElementById("search_status");
- prev_page_link = document.getElementById("prev_page_link");
- next_page_link = document.getElementById("next_page_link");
+ pre_query_label_line = document.getElementById("pre_query_label");
+ prev_page_link1 = document.getElementById("prev_page_link1");
+ prev_page_link2 = document.getElementById("prev_page_link2");
+ next_page_link1 = document.getElementById("next_page_link1");
+ next_page_link2 = document.getElementById("next_page_link2");
// result_links is the array of result link pairs
result_links = new Array();
n = document.getElementById("search_result");
@@ -257,8 +311,20 @@ function MinComparesRx(pats, str) {
}
function NormalizeSpaces(str) {
- return str.replace(/\s\s*/g," ") // single spaces
- .replace(/^ /,"").replace(/ $/,""); // trim edge spaces
+ // use single spaces first, then trim edge spaces
+ return str.replace(/\s\s*/g," ").replace(/^ /,"").replace(/ $/,"");
+}
+
+function SanitizeHTML(str) {
+ // Minimal protection against bad html strings
+ // HACK: we don't want to actually parse these things, but we do want a way
+ // to have tt text, so use a "{{...}}" markup for that.
+ return str.replace(/[&]/g, "&")
+ .replace(/>/g, ">")
+ .replace(/")
+ .replace(/}}/g, " ");
}
function UrlToManual(url) {
@@ -387,6 +453,34 @@ var search_data; // pre-filtered searchable index data
function PreFilter() {
pre_query = NormalizeSpaces(pre_query);
search_data = Search(plt_search_data, pre_query, true, false)[1];
+ if (pre_query == "") {
+ pre_query_label_line.innerHTML =
+ ''
+ +'[set context] ';
+ } else {
+ pre_query_label_line.innerHTML =
+ 'Context: '
+ + (((pre_query_label != "") && pre_query_label)
+ ? SanitizeHTML(pre_query_label)
+ : ('“' + SanitizeHTML(pre_query) + '”'))
+ + ' '
+ +'[clear '
+ +'/'
+ +''
+ +'modify] ';
+ }
last_search_term = null;
last_search_term_raw = null;
}
@@ -459,11 +553,12 @@ function UpdateResults() {
for (var j=0; j'
+ desc[j] + '';
} else if (desc == "module") {
@@ -475,9 +570,10 @@ function UpdateResults() {
note = (note ? (note + " ") : "");
note += 'in '
+ ''
+ ((typeof idx == "number")
? (''+UncompactHtml(search_data[idx][2])+' ')
@@ -509,6 +605,7 @@ function UpdateResults() {
+ ''
+ '(Make sure your spelling is correct'
+ (last_search_term.search(/ /)>=0 ? ', or try fewer keywords' : '')
+ + ((pre_query != "") ? ', or clear the search context' : '')
+ ')
';
} else if (search_results.length <= results_num)
status_line.innerHTML = "Showing all matches" + exact;
@@ -520,9 +617,9 @@ function UpdateResults() {
+ exact
+ " of " + search_results.length
+ ((search_results.length==search_data.length) ? "" : " matches");
- prev_page_link.style.color =
+ prev_page_link1.style.color = prev_page_link2.style.color =
(first_search_result-results_num >= 0) ? "black" : "#e0e0e0";
- next_page_link.style.color =
+ next_page_link1.style.color = next_page_link2.style.color =
(first_search_result+results_num < search_results.length)
? "black" : "#e0e0e0";
saved_status = false;
@@ -575,17 +672,22 @@ function HandleKeyEvent(event) {
}
key_handler = HandleKeyEvent;
-// use this one to set the query field without jumping to the current
-// url again, since some browsers will reload the whole page for that
-// (it would be nice if there was a way to add it to the history too)
-function NewQuery(node) {
- var m = node.href.search(/[?]q=[^?&;]+$/);
- if (m < 0) return true;
- else {
- query.value = decodeURIComponent(node.href.substring(m+3));
+// use this one to set the query field without jumping to the current url
+// again, since some browsers will reload the whole page for that (it would be
+// nice if there was an easy way to add it to the history too)
+function NewQuery(node,label) {
+ var m, href = node.href;
+ if ((m = href.search(/[?]q=[^?&;]+$/)) >= 0) { // `q' cannot be empty
+ query.value = decodeURIComponent(href.substring(m+3));
query.focus();
DoSearch();
return false;
+ } else if ((m = href.search(/[?]hq=[^?&;]*$/)) >= 0) { // `hq' can
+ SetPreQuery(decodeURIComponent(href.substring(m+4)),
+ decodeURIComponent(label));
+ return false;
+ } else {
+ return true;
}
}
new_query = NewQuery;
@@ -599,7 +701,7 @@ function RefineQuery(node) {
m = decodeURIComponent(node.href.substring(m+3));
if (query.value.indexOf(m) >= 0) return true;
else {
- query.value = m + " " + query.value;
+ query.value = query.value + " " + m;
query.focus();
DoSearch();
return false;
@@ -609,8 +711,10 @@ refine_query = RefineQuery;
var panel_shown = false;
function TogglePanel(name) {
- if (panel_shown)
+ if (panel_shown) {
document.getElementById(panel_shown+"_panel").style.display = "none";
+ document.getElementById("close_panel").style.display = "none";
+ }
panel_shown = ((panel_shown != name) && name);
if (panel_shown == "prefs") {
document.getElementById("pre_query_pref").value = pre_query;
@@ -620,9 +724,13 @@ function TogglePanel(name) {
document.getElementById("results_num_pref").value = results_num;
document.getElementById("type_delay_pref").value = type_delay;
document.getElementById("highlight_color_pref").value = highlight_color;
+ } else if (panel_shown == "contexts") {
+ document.getElementById("context_query_pref").value = pre_query;
}
- if (panel_shown)
+ if (panel_shown) {
document.getElementById(panel_shown+"_panel").style.display = "block";
+ document.getElementById("close_panel").style.display = "block";
+ }
}
toggle_panel = TogglePanel;
@@ -643,15 +751,23 @@ function SetShowManuals(inp) {
}
set_show_manuals = SetShowManuals;
-function SetPreQuery(inp) {
- if (inp.value != pre_query) {
- pre_query = inp.value;
+function SetPreQuery(inp,label) {
+ // can be called with the input object, or with a string
+ if (typeof inp != "string") inp = inp.value;
+ if (inp != pre_query) {
+ pre_query = inp;
SetCookie("PLT_PreQuery", pre_query);
+ label = label || "";
+ pre_query_label = label;
+ SetCookie("PLT_PreQueryLabel",label);
PreFilter();
+ document.getElementById("pre_query_pref").value = pre_query;
+ document.getElementById("context_query_pref").value = pre_query;
DoSearch();
}
}
-set_pre_query = SetPreQuery;
+set_pre_query = SetPreQuery;
+set_context_query = SetPreQuery; // a different widget, same effect
function SetShowManuals(inp) {
if (inp.selectedIndex != show_manuals) {