[isabelle-dev] time specifications

[Makarius]

Concerning the question how to specify timeouts etc. in Isabelle, I have 
spent some time investigating the situation of how 
Isabelle/PGIP/ProofGeneral treat preferences, which is important here 
since common configuration options often become system preferences at some 
later stage.

It has turned out resonably easy to support floating point numbers in 
addition to integers.  These changes are already published, see 
Isabelle/ac4d75f86d97 and a few earlier changesets. Note that floats are 
useful independently of the current issue of time.

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.)

The scheme of seconds as float addresses the intuition of at least 3 
others on this thread, as well as Jasmin's requirement to re-scale 
numbers.

It only makes sense to make this move, if we arrive at a single standard 
in the end, instead of four of them.


 	Makarius