[isabelle-dev] time specifications
makarius at sketis.net
Tue Nov 2 17:30:07 CET 2010
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.
More information about the isabelle-dev