less verbose tracing;
authorwenzelm
Fri Feb 18 16:11:58 2011 +0100 (2011-02-18)
changeset 417763bd83302a3c3
parent 41775 6214816d79d3
child 41777 1f7cbe39d425
less verbose tracing;
src/Pure/Concurrent/future.ML
src/Pure/goal.ML
     1.1 --- a/src/Pure/Concurrent/future.ML	Fri Feb 18 16:07:32 2011 +0100
     1.2 +++ b/src/Pure/Concurrent/future.ML	Fri Feb 18 16:11:58 2011 +0100
     1.3 @@ -203,7 +203,7 @@
     1.4        Task_Queue.running task (fn () =>
     1.5          setmp_worker_task task (fn () =>
     1.6            fold (fn job => fn ok => job valid andalso ok) jobs true) ());
     1.7 -    val _ = Multithreading.tracing 1 (fn () =>
     1.8 +    val _ = Multithreading.tracing 2 (fn () =>
     1.9        let
    1.10          val s = Task_Queue.str_of_task task;
    1.11          fun micros time = string_of_int (Time.toNanoseconds time div 1000);
     2.1 --- a/src/Pure/goal.ML	Fri Feb 18 16:07:32 2011 +0100
     2.2 +++ b/src/Pure/goal.ML	Fri Feb 18 16:11:58 2011 +0100
     2.3 @@ -115,7 +115,7 @@
     2.4      let
     2.5        val n = m + i;
     2.6        val _ =
     2.7 -        Multithreading.tracing 1 (fn () =>
     2.8 +        Multithreading.tracing 2 (fn () =>
     2.9            ("PROOFS " ^ Time.toString (Time.now ()) ^ ": " ^ string_of_int n));
    2.10      in n end);
    2.11