static private final String replaceWhiteSpace(String s) {
    int len = s.length();
    for (int i = 0; i < len; i++)
      switch (s.charAt(i)) {
      case '\r':
      case '\n':
      case '\t':
	{
	  char[] buf = s.toCharArray();
	  buf[i] = ' ';
	  for (++i; i < len; i++)
	    switch (buf[i]) {
	    case '\r':
	    case '\n':
	    case '\t':
	      buf[i] = ' ';
	    }
	  return new String(buf);
	}
      }
    return s;
  }