Scribble search, etc.: fix URL decoding

Use Javascript's decodeURIComponent() instead of unescape().

This repair makes searching for Unicode characters work from DrRacket
(e.g., via F1).

original commit: d1525edf62a1db2ade3c64dd17eb81bff87a4112
This commit is contained in:
Matthew Flatt 2014-05-11 07:45:25 -06:00
parent 2a67912028
commit 96fc0407d0

View File

@ -20,7 +20,7 @@ var page_args =
function GetPageArg(key, def) { function GetPageArg(key, def) {
for (var i=0; i<page_args.length; i++) for (var i=0; i<page_args.length; i++)
if (page_args[i][0] == key) return unescape(page_args[i][1]); if (page_args[i][0] == key) return decodeURIComponent(page_args[i][1]);
return def; return def;
} }
@ -131,7 +131,7 @@ function DoSearchKey(event, field, ver, top_path) {
if (event && event.keyCode == 13) { if (event && event.keyCode == 13) {
var u = GetCookie("PLT_Root."+ver, null); var u = GetCookie("PLT_Root."+ver, null);
if (u == null) u = top_path; // default: go to the top path if (u == null) u = top_path; // default: go to the top path
u += "search/index.html?q=" + escape(val); u += "search/index.html?q=" + encodeURIComponent(val);
u = MergePageArgsIntoUrl(u); u = MergePageArgsIntoUrl(u);
location = u; location = u;
return false; return false;