More systematic approach to unicode character replacement.

Author: shans

respec/respec.js

@@ -1750,14 +1750,7 @@ berjon.respec.prototype = {
         s = s.replace(/>/g,'>');
         s = s.replace(/"/g,'"');
         s = s.replace(/</g,'&lt;');
-        s = s.replace(/\u2014/g, '&amp;mdash;');
-        s = s.replace(/\u2018/g, '&amp;lsquo;');
-        s = s.replace(/\u2019/g, '&amp;rsquo;');
-        s = s.replace(/\u00d7/g, '&amp;#xd7;');
-        s = s.replace(/\u2265/g, '&amp;ge;');
-        s = s.replace(/\u03C0/g, '&amp;pi;');
-        s = s.replace(/\u2718/g, '&amp;#x2718;');
-        s = s.replace(/\u2714/g, '&amp;#x2714;');
+	s = s.replace(/([\u0080-\u3000])/g, function(match) { return '&amp;#x' + match.charCodeAt(0).toString(16); });
         return s;
     }
 };