src/Pure/Concurrent/task_queue.ML
changeset 62663 bea354f6ff21
parent 60610 f52b4b0c10c4
child 62819 d3ff367a16a0
--- a/src/Pure/Concurrent/task_queue.ML	Thu Mar 17 16:56:44 2016 +0100
+++ b/src/Pure/Concurrent/task_queue.ML	Fri Mar 18 16:26:35 2016 +0100
@@ -394,4 +394,10 @@
         | NONE => ((NONE, deps'), queue)))
   end;
 
+
+(* toplevel pretty printing *)
+
+val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o Pretty.str o str_of_task);
+val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o Pretty.str o str_of_group);
+
 end;