src/Pure/Concurrent/task_queue.ML
changeset 62819 d3ff367a16a0
parent 62663 bea354f6ff21
child 62826 eb94e570c1a4
equal deleted inserted replaced
62818:2733b240bfea 62819:d3ff367a16a0
   395   end;
   395   end;
   396 
   396 
   397 
   397 
   398 (* toplevel pretty printing *)
   398 (* toplevel pretty printing *)
   399 
   399 
   400 val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o Pretty.str o str_of_task);
   400 val _ = ML_system_pp (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);
   401 val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o Pretty.str o str_of_group);
   402 
   402 
   403 end;
   403 end;