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