src/HOL/Tools/Sledgehammer/async_manager.ML
changeset 47945 4073e51293cf
parent 47529 5f35a95c0645
child 48319 340187063d84
equal deleted inserted replaced
47944:e6b51fab96f7 47945:4073e51293cf
   119                                      postponed_messages store))
   119                                      postponed_messages store))
   120   |> map (fn (_, (tool, (worker, work))) => ((tool, work), worker))
   120   |> map (fn (_, (tool, (worker, work))) => ((tool, work), worker))
   121   |> AList.group (op =)
   121   |> AList.group (op =)
   122   |> List.app (fn ((tool, work), workers) =>
   122   |> List.app (fn ((tool, work), workers) =>
   123                   tool ^ ": " ^
   123                   tool ^ ": " ^
   124                   implode_message (workers |> sort string_ord, work)
   124                   implode_message (workers |> sort_distinct string_ord, work)
   125                   |> break_into_chunks
   125                   |> break_into_chunks
   126                   |> List.app Output.urgent_message)
   126                   |> List.app Output.urgent_message)
   127 
   127 
   128 fun check_thread_manager () = Synchronized.change global_state
   128 fun check_thread_manager () = Synchronized.change global_state
   129   (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
   129   (fn state as {manager, timeout_heap, active, canceling, messages, store} =>