javac Pretty.java should detect when JCIdentifiers contain non-standard characters (as might have been entered with an exotic identifier) and should use the exotic identifier syntax to display such identifiers.