svoid shrinkStringBufferIf50PercentSlack(StringBuffer buf) {
  if (buf == null) ret;
  synchronized(buf) {
    if (buf.capacity() >= buf.length()*2)
      buf.trimToSize();
  }
}