[isabelle-dev] NEWS

[Tjark Weber]

On Fri, 2010-10-29 at 17:48 +0200, Makarius wrote:
> > Unless I have a lapse of memory, the timeout specifications for s/h and 
> > Nitpick are also in seconds, possibly with an "s" appended. As a user I 
> > am glad about that, because I do not think in ms and would not like to 
> > write 30000 instead of 30.
> 
> I have forgotten to say that Jasmin has his own (complicated) time 
> formats.

I find "30 s" and "500 ms" rather intuitive.

Various GNU tools that take time arguments follow a similar convention.
For instance, "man timeout" on my system shows

  timeout [OPTION] NUMBER[SUFFIX] COMMAND [ARG]...

  Start COMMAND, and kill it if still running after NUMBER seconds. SUF-
  FIX may be ‘s’ for seconds (the default),  ‘m’  for  minutes,  ‘h’ for
  hours or ‘d’ for days.

Add a 'ms' suffix, and you have a rather flexible and reasonably
user-friendly input format.

Translating every time into milliseconds internally is fine, of course.
But only supporting milliseconds in the user interface would be awkward.

Just my 2 cents ...

Regards,
Tjark