[m-rev.] for review: Java implementation of time library updated

[James Goddard]

Estimated hours taken: 9
Branches: main

Implemented some library functions for the time library in java.

library/time.m:
	Foreign type "time_t_rep" implemented as instances of "java.util.Date".

	Implemented the following predicates in java:

		time__c_time/3
		time__time_t_is_invalid/1
		time__c_difftime/3
		time__c_localtime/10
		time__c_gmtime/10
		time__c_mktime/10


diff -u time.m time.m
--- time.m	16 Dec 2003 02:57:39 -0000
+++ time.m	16 Dec 2003 05:49:35 -0000
@@ -384,13 +384,7 @@
 	time__c_time(Ret::out, _IO0::di, _IO::uo),
 	[will_not_call_mercury, promise_pure, tabled_for_io],
 "
-	// Milliseconds should be discarded so that
-	//	mktime(localtime(Time)) == Time
-
-	java.util.GregorianCalendar gc = new java.util.GregorianCalendar();
-	gc.set(java.util.Calendar.MILLISECOND, 0);
-
-	Ret = gc.getTime();
+	Ret = new java.util.Date();
 ").
 
 :- pred time__time_t_is_invalid(time_t_rep).
@@ -732,13 +726,16 @@
 
 	Time = gc.getTime();
 
-	// Correct for DST:  This is only an issue for 2 hours of the year.
+	// Correct for DST:  This is only an issue when it is possible for the
+	// same 'time' to occur twice due to daylight savings ending.
 	// (In Melbourne, 2:00am-2:59am occur twice when leaving DST)
 
 	// If the time we constructed is not in daylight savings time, but
-	// it should be, we need to subtract 1 hour.
+	// it should be, we need to subtract the DSTSavings.
 	if (N == 1 && gc.getTimeZone().inDaylightTime(Time) == false) {
-		Time.setTime(Time.getTime() - 3600000);
+		Time.setTime(Time.getTime() -
+				((java.util.SimpleTimeZone) gc.getTimeZone()).
+				getDSTSavings());
 		if (gc.getTimeZone().inDaylightTime(Time) == false) {
 			throw new RuntimeException(
 				""time__mktime: failed to correct for DST"");
@@ -746,9 +743,11 @@
 	}
 
 	// If the time we constructed is in daylight savings time, but
-	// should not be, we need to add 1 hour.
+	// should not be, we need to add the DSTSavings.
 	if (N == 0 && gc.getTimeZone().inDaylightTime(Time) == true) {
-		Time.setTime(Time.getTime() + 3600000);
+		Time.setTime(Time.getTime() +
+				((java.util.SimpleTimeZone) gc.getTimeZone()).
+				getDSTSavings());
 		if (gc.getTimeZone().inDaylightTime(Time) == true) {
 			throw new RuntimeException(
 				""time__mktime: failed to correct for DST"");
--------------------------------------------------------------------------
mercury-reviews mailing list
post:  mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------