# HG changeset patch
# User wenzelm
# Date 1220972388 -7200
# Node ID 8e8313aededc07eecf1dcb02f1951e60bf006c90
# Parent  e56b8b044befb3f7d7ac7e69a45556a2d897c816
human-readable printing of TaskQueue.task/group;

diff -r e56b8b044bef -r 8e8313aededc src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Tue Sep 09 16:35:57 2008 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Tue Sep 09 16:59:48 2008 +0200
@@ -10,6 +10,8 @@
   eqtype task
   eqtype group
   val new_group: unit -> group
+  val str_of_task: task -> string
+  val str_of_group: group -> string
   type queue
   val empty: queue
   val enqueue: group -> task list -> (bool -> bool) -> queue -> task * queue
@@ -28,6 +30,9 @@
 datatype group = Group of serial;
 fun new_group () = Group (serial ());
 
+fun str_of_task (Task i) = string_of_int i;
+fun str_of_group (Group i) = string_of_int i;
+
 
 (* jobs *)
 
diff -r e56b8b044bef -r 8e8313aededc src/Pure/pure_setup.ML
--- a/src/Pure/pure_setup.ML	Tue Sep 09 16:35:57 2008 +0200
+++ b/src/Pure/pure_setup.ML	Tue Sep 09 16:59:48 2008 +0200
@@ -28,6 +28,8 @@
 
 (* ML toplevel pretty printing *)
 
+install_pp (make_pp ["TaskQueue", "task"] (Pretty.pprint o Pretty.str o TaskQueue.str_of_task));
+install_pp (make_pp ["TaskQueue", "group"] (Pretty.pprint o Pretty.str o TaskQueue.str_of_group));
 install_pp (make_pp ["Position", "T"] (Pretty.pprint o Pretty.enum "," "{" "}" o
   map (fn (x, y) => Pretty.str (x ^ "=" ^ y)) o Position.properties_of));
 install_pp (make_pp ["Thm", "thm"] ProofDisplay.pprint_thm);