public static String gettext(AttributedCharacterIterator s) {
	StringBuilder tbuf = new StringBuilder();
	for(int i = s.getBeginIndex(); i < s.getEndIndex(); i++)
	    tbuf.append(s.setIndex(i));
	return(tbuf.toString());
    }