private String format_raw(JCDiagnostic d) {
        DiagnosticSource source = d.getDiagnosticSource();
        int position = d.getIntPosition();

        StringBuilder sb = new StringBuilder();
        if (position == Position.NOPOS)
            sb.append("-");
        else {
            sb.append(source.getName() + ":" + source.getLineNumber(position) + ":" + source.getColumnNumber(position) + ":");
        }
        sb.append(" ");
        sb.append(d.getCode());
        String sep = ": ";
        for (Object arg: d.getArgs()) {
            sb.append(sep);
            if (arg instanceof JCDiagnostic) {
                sb.append('(');
                sb.append(format_raw((JCDiagnostic) arg));
                sb.append(')');
            }
            else if (arg instanceof BaseFileObject)
                sb.append(((BaseFileObject) arg).getShortName());
            else if (arg instanceof JavaFileObject)
                sb.append(BaseFileObject.getSimpleName((JavaFileObject) arg));
            else
                sb.append(arg);
            sep = ", ";
        }
        return sb.toString();
    }