sS hjs_htmlencode() {
  ret hjavascript([[
    function htmlencode(str) {
      return str.replace(/&/g,'&amp;').replace(/</g,'&lt;').replace(/>/g,'&gt;') ;
    }
  ]]);
}