src/Pure/ML-Systems/multithreading_polyml.ML
changeset 40301 bf39a257b3d3
parent 39616 8052101883c3
child 40748 591b6778d076
     1.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Nov 02 20:31:46 2010 +0100
     1.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Nov 02 20:55:12 2010 +0100
     1.3 @@ -120,10 +120,10 @@
     1.4  fun tracing_time detailed time =
     1.5    tracing
     1.6     (if not detailed then 5
     1.7 -    else if Time.>= (time, Time.fromMilliseconds 1000) then 1
     1.8 -    else if Time.>= (time, Time.fromMilliseconds 100) then 2
     1.9 -    else if Time.>= (time, Time.fromMilliseconds 10) then 3
    1.10 -    else if Time.>= (time, Time.fromMilliseconds 1) then 4 else 5);
    1.11 +    else if Time.>= (time, seconds 1.0) then 1
    1.12 +    else if Time.>= (time, seconds 0.1) then 2
    1.13 +    else if Time.>= (time, seconds 0.01) then 3
    1.14 +    else if Time.>= (time, seconds 0.001) then 4 else 5);
    1.15  
    1.16  fun real_time f x =
    1.17    let
    1.18 @@ -202,13 +202,13 @@
    1.19                Posix.Signal.int)
    1.20        | NONE => ())
    1.21        handle OS.SysErr _ => () | IO.Io _ =>
    1.22 -        (OS.Process.sleep (Time.fromMilliseconds 100); if n > 0 then kill (n - 1) else ());
    1.23 +        (OS.Process.sleep (seconds 0.1); if n > 0 then kill (n - 1) else ());
    1.24  
    1.25      val _ =
    1.26        while ! result = Wait do
    1.27          let val res =
    1.28            sync_wait (SOME orig_atts)
    1.29 -            (SOME (Time.+ (Time.now (), Time.fromMilliseconds 100))) cond lock
    1.30 +            (SOME (Time.+ (Time.now (), seconds 0.1))) cond lock
    1.31          in if Exn.is_interrupt_exn res then kill 10 else () end;
    1.32  
    1.33      (*cleanup*)