On Tue, 2 Nov 2010, Makarius wrote:
We can now move forward to standardize time specifications as follows:
* Time is in seconds, as double precision floating point; users can
write 1 or 1.0 or 1.5 etc.
* A one-line function ML seconds: real -> Time.time deflates the
many variations of Time.fromFoo (typical bulky NJ library design).
* ISABELLE_HOME_USER acquires an extra prefix for *named* distributions,
i.e. official releases or bightly builds (not compilations from the
repository) to allow changing the meaning of former
settings in milliseconds. (This helps robustness of installations in
general, not just for timeouts.)
There are still some fine points missing, but those using seconds as
integers can easily upgrade to floats now, using the ML function called
"seconds" together with Attrib.config_real or Parse.real.
Also note that string_of_real helps to print reals in a simple way
(without having to specify custom formats).
Makarius
_______________________________________________
Isabelle-dev mailing list
Isabelle-dev@mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
