[isabelle-dev] time specifications

[Makarius]

On Tue, 2 Nov 2010, Jasmin Christian Blanchette wrote:

> Am 02.11.2010 um 14:08 schrieb Makarius:
>
> 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.

The above 1.5 was indeed hardly possible before my recent introduction of 
floating point as native outer syntax tokens, and might be the best 
posthoc explanation for your format of "s" and "ms".

Now (e.g. in version c753e3f8b4d6) you can use Parse.real to get the 
result of the user using either integer or float notation.  The 
Attrib.config_real also does that internally.


 	Makarius