# HG changeset patch
# User blanchet
# Date 1284485898 -7200
# Node ID 8e585c7d418a0677e9bd4db6ba74f47ac25e860a
# Parent  f661064b2b8022383e2da30c157d9916787fd1a7
export function

diff -r f661064b2b80 -r 8e585c7d418a src/HOL/Tools/async_manager.ML
--- a/src/HOL/Tools/async_manager.ML	Tue Sep 14 17:36:27 2010 +0200
+++ b/src/HOL/Tools/async_manager.ML	Tue Sep 14 19:38:18 2010 +0200
@@ -8,6 +8,7 @@
 
 signature ASYNC_MANAGER =
 sig
+  val break_into_chunks : string list -> string list
   val launch :
     string -> Time.time -> Time.time -> string -> (unit -> string) -> unit
   val kill_threads : string -> string -> unit
@@ -94,8 +95,7 @@
 
 (* This is a workaround for Proof General's off-by-a-few sendback display bug,
    whereby "pr" in "proof" is not highlighted. *)
-fun break_into_chunks xs =
-  maps (space_explode "\000" o replace_all "\n\n" "\000" o snd) xs
+val break_into_chunks = maps (space_explode "\000" o replace_all "\n\n" "\000")
 
 fun print_new_messages () =
   case Synchronized.change_result global_state
@@ -104,7 +104,7 @@
                                    store)) of
     [] => ()
   | msgs as (tool, _) :: _ =>
-    let val ss = break_into_chunks msgs in
+    let val ss = break_into_chunks (map snd msgs) in
       List.app priority (tool ^ ": " ^ hd ss :: tl ss)
     end
 
@@ -229,6 +229,9 @@
       "Recent " ^ worker ^ " messages" ^
         (if length tool_store <= limit then ":"
          else " (" ^ string_of_int limit ^ " displayed):");
-  in List.app priority (header :: break_into_chunks (#1 (chop limit tool_store))) end
+  in
+    List.app priority (header :: break_into_chunks
+                                     (map snd (#1 (chop limit tool_store))))
+  end
 
 end;