All purpose String trimmer

The java string class supports a trim() operation that trims ' '. You may find that you want to trim another character. This terse example will trim any character from the beginning and end of a String. It is based on the JDK's trim() method with a few more attempts at brevity.

   public static String trim(String source, char c) {
      int len = source.length();
      int st = 0;
      char[] val = source.toCharArray();
      for (;(st < len) && (val[st] <= c);st++){}
      for (;(st < len) && (val[len-1]<=c);len--){}
      return ((st > 0) || (len < source.length())) ? 
         source.substring(st, len) : source;
   }