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 _______________________________________________ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev