[isabelle-dev] NEWS

[Makarius]

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