- public String toString() {
- StringBuffer ret = new StringBuffer();
- for(int i=0; i<children.length; i++) {
- String q = children[i]==null ? "null" : children[i].toString();
- if (q.length() > 0) { ret.append(q); ret.append(" "); }
- }
- String tail = ret.toString().trim();
- String h = (head!=null && !head.toString().equals("")) ? (tail.length() > 0 ? head+":" : head+"") : "";
- if (tail.length() > 0) tail = "{" + tail + "}";
- return h + tail;
+ protected String headToString() { return head==null?null:head.toString(); }
+ protected String headToJava() { return head==null?null:StringUtil.toJavaString(head+""); }
+ protected String left() { return "{"; }
+ protected String right() { return "}"; }
+ protected boolean ignoreSingleton() { return false; }
+
+ public GraphViz.Node toGraphViz(GraphViz gv) {
+ if (gv.hasNode(this)) return gv.createNode(this);
+ GraphViz.Node n = gv.createNode(this);
+ n.label = head()==null ? "" : head().toString();
+ //n.color = "red";
+ for(Tree t : this) n.edge(t, null);
+ return n;