// automagically encode a whole map (keys+values)
static Map htmlencode(Map o) {
  new HashMap bla;
  for (O key : keys(o)) {
    O value = o.get(key);
    bla.put(htmlencode(key), htmlencode(value));
  }
  ret bla;
}

static String htmlencode(Object o) {
  ret htmlencode(string(o));
}

static String htmlencode(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 >= 0x100)
        out.append("&#x").append(charToHex(c)).append(';');
      else if (c > 127 || c == '"' || c == '<' || c == '>' || c == '&') {
          out.append("&#");
          out.append((int) c);
          out.append(';');
      } else
          out.append(c);
  }
  ret out.toString();
}