d6b0dfcd04
Also switches scribble search trampoline to standard DOCTYPE. Scribble's HTML output currently relies on the quirks-mode box model for layout of the many tables used in rendering. However, Scribble doesn't need the rest of the changes in browser quirks modes, so we choose a DOCTYPE that just changes the box model. It's non-obvious how to replicated this formatting with CSS in standard-mode rendering. Probably a better long term solution is to move away from table-based layout. See further discussion on GitHub pull request 158 here: https://github.com/plt/racket/pull/158
48 lines
1.6 KiB
HTML
48 lines
1.6 KiB
HTML
<!DOCTYPE html>
|
|
<html>
|
|
<!--
|
|
This page serves as a trampoline - it finds an "hq" parameter,
|
|
stores it in a cookie, and continues to the search page. This
|
|
avoids having the "hq" argument be on the search page - since then
|
|
when you refresh the search you will reset the cookie.
|
|
-->
|
|
<head>
|
|
<meta http-equiv="content-type" content="text/html; charset=utf-8" />
|
|
<title>Search Manuals</title>
|
|
<script type="text/javascript" src="../scribble-common.js"></script>
|
|
</head>
|
|
<body>
|
|
<noscript>Sorry, you must have JavaScript to use this page.<br></noscript>
|
|
<script>
|
|
|
|
if (location.search.length > 0) {
|
|
var paramstrs = location.search.substring(1).split(/[;&]/);
|
|
var newsearch = null;
|
|
for (var i=0; i<paramstrs.length; i++) {
|
|
var param = paramstrs[i].split(/=/);
|
|
// an empty "hq=" can be used to clear the cookie
|
|
if (param[0] == "hq") {
|
|
SetCookie("PLT_ContextQuery",
|
|
((param.length==2) ? unescape(param[1]) : ""));
|
|
} else if (param[0] == "label") {
|
|
SetCookie("PLT_ContextQueryLabel",
|
|
((param.length==2) ? unescape(param[1]) : ""));
|
|
} else {
|
|
newsearch = (newsearch == null)
|
|
? paramstrs[i] : (newsearch + "&" + paramstrs[i]);
|
|
}
|
|
}
|
|
newsearch = (newsearch == null) ? "" : ("?" + newsearch);
|
|
// localtion.replace => jump without leaving the current page in the history
|
|
// (the new url uses "index.html" and the new search part)
|
|
location.replace(location.href.replace(/\/[^\/?#]*[?][^#]*/,
|
|
"/index.html" + newsearch));
|
|
} else {
|
|
// no parameters found? just jump to the search page...
|
|
location.href = "index.html";
|
|
}
|
|
|
|
</script>
|
|
</body>
|
|
</html>
|