public String toString() {
        if (defaultFormatter == null) {
            defaultFormatter =
                new DiagnosticFormatter();
        }
        return defaultFormatter.format(this);
    }