+ public String getName() {
+ if (name != null) return name;
+ return "(anon_union)";
+ }
+ public String toString() {
+ if (name != null) return name;
+ StringBuffer sb = new StringBuffer();
+ sb.append("(");
+ bodyToString(sb, "", " | ");
+ sb.append(")");
+ return sb.toString();
+ }