[isabelle-dev] NEWS

[Makarius]

On Fri, 29 Oct 2010, Lukas Bulwahn wrote:

> * Quickcheck now has a configurable time limit which is set to 30 
> seconds by default. This can be changed by adding [timeout = n] to the 
> quickcheck command. The time limit for auto quickcheck is still set 
> independently, by default to 5 seconds.

I am a bit puzzled about the unit of seconds here. When time is 
represented as plain integer in Isabelle, it is usually done in 
milliseconds.  This is motivated by simplicity and portability.

Milliseconds basically give 3 digits of fixed-point representation without 
venturing on floating point numbers or SML's complicated time datatype, or 
even more complicated languages for time spans (like the Babylonians 
invented a long time ago to make life more interesting). Also note that 
configuration options are often correlated with preferences, which need to 
be manageable outside the ML process (e.g. in PG/Emacs or Isabelle/Scala). 
So any extra complications of ML time formats would also affect other 
environments.

The JVM normally observes our milliseconds standard as well, and jEdit 
properties follow the same.  This makes Isabelle/ML, Isabelle/Scala, 
Isabelle/jEdit agree nicely without any further ado.


 	Makarius