src/Pure/Concurrent/task_queue.ML
changeset 62826 eb94e570c1a4
parent 62819 d3ff367a16a0
child 62891 7a11ea5c9626
     1.1 --- a/src/Pure/Concurrent/task_queue.ML	Sat Apr 02 23:14:08 2016 +0200
     1.2 +++ b/src/Pure/Concurrent/task_queue.ML	Sat Apr 02 23:29:05 2016 +0200
     1.3 @@ -139,7 +139,7 @@
     1.4      let
     1.5        val start = Time.now ();
     1.6        val result = Exn.capture (restore_attributes e) ();
     1.7 -      val t = Time.- (Time.now (), start);
     1.8 +      val t = Time.now () - start;
     1.9        val _ = (case timing of NONE => () | SOME var => Synchronized.change var (update t));
    1.10      in Exn.release result end) ();
    1.11  
    1.12 @@ -167,14 +167,14 @@
    1.13  (* timing *)
    1.14  
    1.15  fun running task =
    1.16 -  update_timing (fn t => fn (a, b, ds) => (Time.+ (a, t), b, ds)) task;
    1.17 +  update_timing (fn t => fn (a, b, ds) => (a + t, b, ds)) task;
    1.18  
    1.19  fun joining task =
    1.20 -  update_timing (fn t => fn (a, b, ds) => (Time.- (a, t), b, ds)) task;
    1.21 +  update_timing (fn t => fn (a, b, ds) => (a - t, b, ds)) task;
    1.22  
    1.23  fun waiting task deps =
    1.24    update_timing (fn t => fn (a, b, ds) =>
    1.25 -    (Time.- (a, t), Time.+ (b, t),
    1.26 +    (a - t, b + t,
    1.27        if ! Multithreading.trace > 0
    1.28        then fold (insert (op =) o name_of_task) deps ds else ds)) task;
    1.29