equal
deleted
inserted
replaced
611 indent(); |
611 indent(); |
612 out.println("]"); |
612 out.println("]"); |
613 return null; |
613 return null; |
614 } |
614 } |
615 |
615 |
|
616 @Override |
|
617 public Void visitSystemProperty(SystemPropertyTree node, Void p) { |
|
618 header(node); |
|
619 indent(+1); |
|
620 print("property name", node.getPropertyName().toString()); |
|
621 indent(-1); |
|
622 indent(); |
|
623 out.println("]"); |
|
624 return null; |
|
625 } |
|
626 |
616 public Void visitText(TextTree node, Void p) { |
627 public Void visitText(TextTree node, Void p) { |
617 header(node, compress(node.getBody())); |
628 header(node, compress(node.getBody())); |
618 return null; |
629 return null; |
619 } |
630 } |
620 |
631 |