String indentStr = "";
StringBuffer b = new StringBuffer();
    public void dump(PrintStream stream, int indent)    {      String indentStr = "";      for (int i = 0; i < indent; ++i)	indentStr += "  ";      dumpElement(stream, indentStr, this);    }