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