src/Pure/Concurrent/future.ML
changeset 32617 bfbdeddc03bc
parent 32616 8ef1aa1cfcc7
child 32644 e4511a1b4c1b
equal deleted inserted replaced
32616:8ef1aa1cfcc7 32617:bfbdeddc03bc
   235             let
   235             let
   236               val {ready, pending, running} = Task_Queue.status (! queue);
   236               val {ready, pending, running} = Task_Queue.status (! queue);
   237               val total = length (! workers);
   237               val total = length (! workers);
   238               val active = count_active ();
   238               val active = count_active ();
   239             in
   239             in
   240               "SCHEDULE " ^ string_of_int (Time.toMilliseconds now) ^ ": " ^
   240               "SCHEDULE " ^ Time.toString now ^ ": " ^
   241                 string_of_int ready ^ " ready, " ^
   241                 string_of_int ready ^ " ready, " ^
   242                 string_of_int pending ^ " pending, " ^
   242                 string_of_int pending ^ " pending, " ^
   243                 string_of_int running ^ " running; " ^
   243                 string_of_int running ^ " running; " ^
   244                 string_of_int total ^ " workers, " ^
   244                 string_of_int total ^ " workers, " ^
   245                 string_of_int active ^ " active"
   245                 string_of_int active ^ " active"