1.1 --- a/src/Pure/Concurrent/future.ML	Sat Jul 18 22:51:29 2009 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Sat Jul 18 22:52:31 2009 +0200
     1.3 @@ -133,7 +133,7 @@
     1.4      val ws = ! workers;
     1.5      val m = string_of_int (length ws);
     1.6      val n = string_of_int (length (filter #2 ws));
     1.7 -  in Multithreading.tracing 1 (fn () => "SCHEDULE: " ^ m ^ " workers, " ^ n ^ " active") end;
     1.8 +  in Multithreading.tracing 2 (fn () => "SCHEDULE: " ^ m ^ " workers, " ^ n ^ " active") end;
     1.9  
    1.10  fun change_active active = (*requires SYNCHRONIZED*)
    1.11    change workers (AList.update Thread.equal (Thread.self (), active));
    1.12 @@ -188,6 +188,15 @@
    1.13  
    1.14  fun scheduler_next () = (*requires SYNCHRONIZED*)
    1.15    let
    1.16 +    (*queue status*)
    1.17 +    val _ = Multithreading.tracing 1 (fn () =>
    1.18 +      let val {ready, pending, running} = Task_Queue.status (! queue) in
    1.19 +        "SCHEDULE: " ^
    1.20 +          string_of_int ready ^ " ready, " ^
    1.21 +          string_of_int pending ^ " pending, " ^
    1.22 +          string_of_int running ^ " running"
    1.23 +      end);
    1.24 +
    1.25      (*worker threads*)
    1.26      val _ =
    1.27        (case List.partition (Thread.isActive o #1) (! workers) of
    1.28 @@ -277,8 +286,8 @@
    1.29  fun get_result x = the_default (Exn.Exn (SYS_ERROR "unfinished future")) (peek x);
    1.30  
    1.31  fun join_wait x =
    1.32 -  while not (is_finished x)
    1.33 -  do SYNCHRONIZED "join_wait" (fn () => wait ());
    1.34 +  if SYNCHRONIZED "join_wait" (fn () => is_finished x orelse (wait (); false))
    1.35 +  then () else join_wait x;
    1.36  
    1.37  fun join_next x = (*requires SYNCHRONIZED*)
    1.38    if is_finished x then NONE