Re: \timing interval

Corey Huinker <corey(dot)huinker(at)gmail(dot)com> writes:
> On Thu, Sep 1, 2016 at 3:01 PM, Tom Lane <tgl(at)sss(dot)pgh(dot)pa(dot)us> wrote:
>> Well, that code's on the backend side so we're not going to just call it
>> in any case. And I think we don't want to be quite so verbose as to go up
>> to hh:mm:ss.fff as soon as we get past 1 second. However, comparing that
>> output to what I had suggests that maybe it's better to keep a leading
>> zero in two-digit fields, that is render times like "00:01.234",
>> "01:23.456", or "01:23:45.678" rather than suppressing the initial zero as
>> I had in my examples. It's an extra character but I think it reinforces
>> the meaning.

> +1
> The larger jump in widths from no MM:SS to HH:MM:SS is a good visual cue.
> Jumping from MM:SS to H:MM:SS to HH:MM:SS would be more subtle and possibly
> confusing.

Attached is an updated patch that does it like that. Sample output
(generated by forcing specific arguments to PrintTiming):

Time: 0.100 ms
Time: 1.200 ms
Time: 1001.200 ms (00:01.001)
Time: 12001.200 ms (00:12.001)
Time: 60001.200 ms (01:00.001)
Time: 720001.200 ms (12:00.001)
Time: 3660001.200 ms (01:01:00.001)
Time: 43920001.200 ms (12:12:00.001)
Time: 176460001.200 ms (2 01:01:00.001)
Time: 216720001.200 ms (2 12:12:00.001)
Time: 8816460001.200 ms (102 01:01:00.001)
Time: 8856720001.200 ms (102 12:12:00.001)

Barring objections I'll commit this soon.

regards, tom lane