Sanitize the output from HTML escape characters.

Noted by ozzloy on IRC.  The search page appears to fail when
searching for the term 'string<?'; in truth, the search succeeds, but
the search link-printing code doesn't escape the '<?' part of the
identifier.

collects/scribblings/main/private/search.js

@@ -643,7 +643,7 @@ function UncompactUrl(url) {
 
 function UncompactHtml(x) {
   if (typeof x == "string") {
-    return x;
+    return SanitizeHTML(x);
   } else if (!(x instanceof Array)) {
     return alert("Internal error in PLT docs");
   } else if ((x.length == 2) && (typeof(x[0]) == "number")) {