JDBC, Timestamps, and Fractions of a Second

I'm using the JDBC2 driver in the PostgreSQL 7.0.1 distribution to both
INSERT and SELECT (the same) records with timestamp columns. The
ResultSet.getTimestamp method is choking, because it's looking for a
"yyyy-MM-dd HH:mm:sszzz" format, while the default in 7.0 now seems to
be "yyyy-MM-dd HH:mm:ss.SSzzz", where "SS" is centiseconds. (The Java 2
SDK javadoc for SimpleDateFormat actually defines 'S' to represent a
millisecond digit in a time pattern string, but I'm using it here for
centiseconds since they define no character for that. :-/ )

Here's part of the stack trace:

Bad Timestamp Format at 19 in 2000-06-14 15:37:11.67-04
at org.postgresql.jdbc2.ResultSet.getTimestamp(ResultSet.java:447)
at org.postgresql.jdbc2.ResultSet.getTimestamp(ResultSet.java:595)

Aleksey Demakov wrote about a similar problem in 1998, (see
http://www.postgresql.org/mhonarc/pgsql-interfaces/1998-10/msg00183.html),
and he rewrote the code to account for milliseconds.

Likewise, I've rewritten the current code to account for both the "no
fractions" format and the "centiseconds" format. The patch is below.

This is solving my immediate problem, but I don't know what other
formats may need to be taken into consideration to make the patch an
acceptably robust solution.

I'd appreciate any comments (e.g. could this patch -- or a more robust
version -- be applied to the next version of the driver? -- I am CCing
this to patches(at)postgres(dot)retep(dot)org(dot)uk).

(As an aside, in the way of trivia, a search of
http://www.dictionary.com turned up no legitimate word "centiseconds."
However, a search on Google confirmed that, correctly or not, others do
use it. :)

Platform info:
-Red Hat Linux 6.2
-Blackdown JDK 1.2.2 RC4

Regards,
Jim Caley
E-mail: caley(at)chesco(dot)com
--

*** ResultSet.java.orig Fri May 12 16:54:22 2000
--- ResultSet.java Tue Jun 13 16:46:21 2000
***************
*** 439,445 ****
if(s==null)
return null;

! SimpleDateFormat df = new SimpleDateFormat("yyyy-MM-dd
HH:mm:sszzz");

try {
return new Timestamp(df.parse(s).getTime());
--- 439,447 ----
if(s==null)
return null;

! SimpleDateFormat df = (s.charAt(19) == '.') ?
! new SimpleDateFormat("yyyy-MM-dd HH:mm:ss.SSzzz") :
! new SimpleDateFormat("yyyy-MM-dd HH:mm:sszzz");

try {
return new Timestamp(df.parse(s).getTime());