diff --git a/collects/scribble/scribble-common.js b/collects/scribble/scribble-common.js
index 507f914fc0..636aee4324 100644
--- a/collects/scribble/scribble-common.js
+++ b/collects/scribble/scribble-common.js
@@ -1,6 +1,6 @@
// Common functionality for PLT documentation pages
-function GetCookie(key) {
+function GetCookie(key, def) {
if (document.cookie.length <= 0) return null;
var cookiestrs = document.cookie.split(/; */);
for (var i in cookiestrs) {
@@ -9,7 +9,7 @@ function GetCookie(key) {
if (eql >= 0 && cur.substring(0,eql) == key)
return unescape(cur.substring(eql+1));
}
- return null;
+ return def;
}
function SetCookie(key, val) {
@@ -28,7 +28,7 @@ function SetPLTRoot(ver, relative) {
// adding index.html works because of the above
function GotoPLTRoot(ver, relative) {
- var u = GetCookie("PLT_Root."+ver);
+ var u = GetCookie("PLT_Root."+ver, null);
if (u == null) return true; // no cookie: use plain up link
// the relative path is optional, default goes to the toplevel start page
if (!relative) relative = "index.html";
@@ -47,7 +47,7 @@ function NormalizePath(path) {
function DoSearchKey(event, field, ver) {
var val = field.value;
if (event && event.keyCode == 13 && val.indexOf("...search...") < 0) {
- var u = GetCookie("PLT_Root."+ver);
+ var u = GetCookie("PLT_Root."+ver, null);
if (u == null) u = "../"; // default: go up
location = u + "search/index.html" + "?q=" + escape(val);
return false;
diff --git a/collects/scribblings/main/private/make-search.ss b/collects/scribblings/main/private/make-search.ss
index 726c460d8e..325bcd3750 100644
--- a/collects/scribblings/main/private/make-search.ss
+++ b/collects/scribblings/main/private/make-search.ss
@@ -122,32 +122,60 @@
@(add-between l ",\n")];
// Globally visible bindings
- var key_handler;
+ var key_handler, toggle_help_pref, hide_prefs,
+ set_results_num, set_highlight_color;
(function(){
// Configuration options
- var results_num = 20;
+ var results_num = (GetCookie("PLT_ResultsNum", false) || 20);
+ var highlight_color = (GetCookie("PLT_HighlightColor", false) || "#ffd");
+ var background_color = "#f8f8f8";
var query, status, results_container, result_links,
- prev_page_link, next_page_link;
+ prev_page_link, next_page_link, panel;
function InitializeSearch() {
var n;
n = document.getElementById("plt_search_container").parentNode;
// hack the table in
n.innerHTML = ''
- +'