1.1 --- a/src/HOL/Tools/atp_manager.ML	Mon Dec 22 14:40:27 2008 +0100
     1.2 +++ b/src/HOL/Tools/atp_manager.ML	Mon Dec 22 16:57:11 2008 +0100
     1.3 @@ -104,39 +104,31 @@
     1.4  val managing_thread = ref (NONE: Thread.thread option);
     1.5  
     1.6  
     1.7 -(* unregister thread from thread manager -- move to cancelling *)
     1.8 +(* unregister thread *)
     1.9  
    1.10  fun unregister (success, message) thread = Synchronized.change_result state
    1.11 -  (fn State {timeout_heap, oldest_heap, active, cancelling, messages} =>
    1.12 -    let
    1.13 -      val info = lookup_thread active thread
    1.14 +  (fn state as State {timeout_heap, oldest_heap, active, cancelling, messages} =>
    1.15 +    (case lookup_thread active thread of
    1.16 +      SOME (birthtime, _, description) =>
    1.17 +        let
    1.18 +          val (group, active') =
    1.19 +            if success then List.partition (fn (_, (tb, _, _)) => tb = birthtime) active
    1.20 +            else List.partition (fn (th, _) => Thread.equal (th, thread)) active
    1.21 +          val others = delete_thread thread group
    1.22  
    1.23 -      (* get birthtime of unregistering thread if successful - for group-killing*)
    1.24 -      val birthtime = case info of NONE => Time.zeroTime
    1.25 -        | SOME (tb, _, _) => if success then tb else Time.zeroTime
    1.26 +          val now = Time.now ()
    1.27 +          val cancelling' =
    1.28 +            fold (fn (th, (tb, _, desc)) => update_thread (th, (tb, now, desc))) others cancelling
    1.29  
    1.30 -      (* move unregistering thread to cancelling *)
    1.31 -      val active' = delete_thread thread active
    1.32 -      val cancelling' = case info of NONE => cancelling
    1.33 -        | SOME (tb, _, desc) => update_thread (thread, (tb, Time.now (), desc)) cancelling
    1.34 -
    1.35 -      (* move all threads of the same group to cancelling *)
    1.36 -      val group_threads = active |> map_filter (fn (th, (tb, _, desc)) =>
    1.37 -          if tb = birthtime then SOME (th, (tb, Time.now (), desc)) else NONE)
    1.38 -      val active'' = filter_out (fn (_, (tb, _, _)) => tb = birthtime) active'
    1.39 -      val cancelling'' = append group_threads cancelling'
    1.40 -
    1.41 -      (* message for user *)
    1.42 -      val message' = case info of NONE => ""
    1.43 -        | SOME (_, _, desc) => "Sledgehammer: " ^ desc ^ "\n" ^ message ^
    1.44 -          (if null group_threads then ""
    1.45 -           else "\nInterrupted " ^ string_of_int (length group_threads - 1) ^ " other group members")
    1.46 -
    1.47 -      val messages' = case info of NONE => messages
    1.48 -        | SOME (_, _, desc) => desc ^ "\n" ^ message ::
    1.49 -           (if length messages <= message_store_limit then messages
    1.50 -            else #1 (chop message_store_limit messages))
    1.51 -    in (message', make_state timeout_heap oldest_heap active'' cancelling'' messages') end);
    1.52 +          val msg = description ^ "\n" ^ message
    1.53 +          val message' = "Sledgehammer: " ^ msg ^
    1.54 +            (if null others then ""
    1.55 +             else "\nInterrupted " ^ string_of_int (length others) ^ " other group members")
    1.56 +          val messages' = msg ::
    1.57 +            (if length messages <= message_store_limit then messages
    1.58 +             else #1 (chop message_store_limit messages))
    1.59 +        in (message', make_state timeout_heap oldest_heap active' cancelling' messages') end
    1.60 +    | NONE => ("", state)));
    1.61  
    1.62  
    1.63  (* kill excessive atp threads *)