// 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 > 127 || c == '"' || c == '<' || c == '>' || c == '&') {
            out.append("&#");
            out.append((int) c);
            out.append(';');
        } else {
            out.append(c);
        }
    }
    return out.toString();
  }