class HTML {
    public static String escape(String s) {
        /*
        Escape a string so it will be interpreted as literal text in HTML.
        */

        char c;
        // resizing the StringBuilder is expensive, so try to make sure we
        // have enough space to start with.
        StringBuilder out = new StringBuilder((int) (s.length()*1.25));
        
        for(int i=0; i<s.length(); i++) {
            c = s.charAt(i);
            switch( c ) {
                case '<':
                    out.append("&lt;");
                    break;
                case '>':
                    out.append("&gt;");
                    break;
                case '&':
                    out.append("&amp;");
                    break;
                case '"':
                    out.append("&quot;");
                    break;
                default:
                    out.append(c);
            }
        }
        return out.toString();
    }

}