On Fri, 29 Oct 2010, Sascha Boehme wrote:
How about providing a parse function "time_of_string" which turns
strings like "30s" or "15ms" into proper times, and possibly adding a
configuration option scheme for times (besides the existing bool, int
and string schemes)? It seems that this could and should be provided be
provided by the system to have a uniform interface and prevent further
confusion.
This is quite natural, but a neither simple nor portable as I've said.
Both Isabelle/ML and Isabelle/Scala need to treat it uniformly, and maybe
other front-ends that inspect externalized Isabelle "preferences" or
"properites".
Unification of divergent developments is very important, but one should
always aim at something more close to the insersection than the union of
accumulated features.
Right now I do not fully understand the existing preference system -- I
need to look at it again when it is officially integrated into
Isabelle/Scala -- so it is hard to say what is the simplest possible
flexible solution. Maybe time in seconds, but as a float, but this is apt
to cause confusion with persistent preferences of users out there.
Makarius
_______________________________________________
Isabelle-dev mailing list
Isabelle-dev@mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
