static S htmlencode_noQuotes(String s) {
  if (s == null) ret "";
  StringBuilder out = new StringBuilder(Math.max(16, s.length()));
  for (int i = 0; i < s.length(); i++) {
    char c = s.charAt(i);
    if (c > 127 || c == '<' || c == '>' || c == '&') {
      out.append("&#");
      out.append((int) c);
      out.append(';');
    } else
      out.append(c);
  }
  ret out.toString();
}