add util function to escape strings for manual building of HTML, and use this for the portal title

fix #319

code/utils_misc.js

@@ -365,6 +365,14 @@ window.escapeJavascriptString = function(str) {
   return (str+'').replace(/[\\"']/g,'\\$&');
 }
 
+//escape special characters, such as tags
+window.escapeHtmlSpecialChars = function(str) {
+  var div = document.createElement(div);
+  var text = document.createTextNode(str);
+  div.appendChild(text);
+  return div.innerHTML;
+}
+
 window.prettyEnergy = function(nrg) {
   return nrg> 1000 ? Math.round(nrg/1000) + ' k': nrg;
 }