src/Pure/Concurrent/task_queue.ML
changeset 62663 bea354f6ff21
parent 60610 f52b4b0c10c4
child 62819 d3ff367a16a0
equal deleted inserted replaced
62662:291cc01f56f5 62663:bea354f6ff21
   392         (case ready_dep Tasks.empty deps' of
   392         (case ready_dep Tasks.empty deps' of
   393           SOME res => result res deps'
   393           SOME res => result res deps'
   394         | NONE => ((NONE, deps'), queue)))
   394         | NONE => ((NONE, deps'), queue)))
   395   end;
   395   end;
   396 
   396 
       
   397 
       
   398 (* toplevel pretty printing *)
       
   399 
       
   400 val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o Pretty.str o str_of_task);
       
   401 val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o Pretty.str o str_of_group);
       
   402 
   397 end;
   403 end;