[isabelle-dev] time specifications

[Jasmin Christian Blanchette]

Am 02.11.2010 um 14:08 schrieb Makarius:

> The scheme of seconds as float addresses the intuition of at least 3 others on this thread, as well as Jasmin's requirement to re-scale numbers.
> 
> It only makes sense to make this move, if we arrive at a single standard in the end, instead of four of them.

Floating-point numbers are a decent alternatives, and seconds, being the standard unit for time in physics and elsewhere, makes sense; hence, I will not stand in the way of standardization. (My personal preference does remain for a unit suffix, e.g., "s", for readability's sake, though.)

A very minor issue is that I was never able to parse options like

    nitpick [timeout = 1.5]

even with custom parsers, unless 1.5 is doubly-quoted. Users might not realize they need quoting and will most probably be confused by the resulting error.

Jasmin