replacement for String.format in GWT?

[Magnus]

Hi,

I need String.format:

String r = String.format("%2d %2d:%2d:%2d",d,h,m,s);

Since GWT does not support this method: What can I do instead?

Magnus

[Ben Imp]

If you are trying to format a date, which appears to be the case, you
can use DateTimeFormat.

-Ben

[Magnus]

Hi,

it's not a date!

I want to format integer numbers with leading "0"s and a fixed number
of digits.

Magnus

[Magnus]

Hi,

I have to explain my real problem with DateFormat:

I need to represent a time span (the time elapsed during a chess
move), not a real date, e. g.:

0000-01-02 03:04:05

means:
0 years, 1 month, 2 days, 3 hours, 4 minutes and 5 seconds.

Such a span is computed by subtracting a date from another date and
stored as a date:

Date d1,d2;
..
long t1 = d1.getTime ();
long t2 = d2.getTime ();
long t = t2 - t1;
Date d = new Date (t);

I cannot format d it with DateFormat, since it is interpreted as an
offset to 1970. If I could supress this interpretation, I would be
glad.

As a workaround, I extracted the date elements as integers and tried
to format them with String.format.

Magnus

[ep]

unfortunately, there is no formatter, I'd also would be happy if there
was one. but you can make a helper function which formats numbers with
padding zeros:

String fn(int num, int pads) {
if(num>=10)return Integer.toString(num);
char[] z;
for(z= new char[pads], int i=0; i<z.length; i++) z[i]='0';
return "" + new String(z) + Integer.toString(num);
}

and then:
{
String str = ""+fn(0,4)+" "+fn(9,1) + " " + fn(12); //would result i n
"0000 09 12"
}

ok, its ugly, but does the job

[Magnus]

Hi,

thanks! It's ugly, but it works.

Magnus