diff -r 325c8fd0d762 -r 340187063d84 src/HOL/Tools/Sledgehammer/async_manager.ML --- a/src/HOL/Tools/Sledgehammer/async_manager.ML Wed Jul 18 08:44:04 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/async_manager.ML Wed Jul 18 08:44:04 2012 +0200 @@ -8,12 +8,12 @@ signature ASYNC_MANAGER = sig - val implode_desc : string * string -> string val break_into_chunks : string -> string list val launch : string -> Time.time -> Time.time -> string * string -> (unit -> bool * string) -> unit val kill_threads : string -> string -> unit + val has_running_threads : string -> bool val running_threads : string -> string -> unit val thread_messages : string -> string -> int option -> unit end; @@ -23,29 +23,27 @@ (** preferences **) -val message_store_limit = 20; -val message_display_limit = 10; +val message_store_limit = 20 +val message_display_limit = 10 (** thread management **) -val implode_desc = op ^ o apfst quote - fun implode_message (workers, work) = - space_implode " " (Try.serial_commas "and" (map quote workers)) ^ work + space_implode " " (Try.serial_commas "and" workers) ^ work (* data structures over threads *) structure Thread_Heap = Heap ( - type elem = Time.time * Thread.thread; - fun ord ((a, _), (b, _)) = Time.compare (a, b); -); + type elem = Time.time * Thread.thread + fun ord ((a, _), (b, _)) = Time.compare (a, b) +) -fun lookup_thread xs = AList.lookup Thread.equal xs; -fun delete_thread xs = AList.delete Thread.equal xs; -fun update_thread xs = AList.update Thread.equal xs; +fun lookup_thread xs = AList.lookup Thread.equal xs +fun delete_thread xs = AList.delete Thread.equal xs +fun update_thread xs = AList.update Thread.equal xs (* state of thread manager *) @@ -65,7 +63,7 @@ canceling = canceling, messages = messages, store = store} val global_state = Synchronized.var "async_manager" - (make_state NONE Thread_Heap.empty [] [] [] []); + (make_state NONE Thread_Heap.empty [] [] [] []) (* unregister thread *) @@ -76,22 +74,23 @@ (case lookup_thread active thread of SOME (tool, _, _, desc as (worker, its_desc)) => let - val active' = delete_thread thread active; + val active' = delete_thread thread active val now = Time.now () val canceling' = (thread, (tool, now, desc)) :: canceling - val message' = (worker, its_desc ^ "\n" ^ message) + val message' = + (worker, its_desc ^ (if message = "" then "" else "\n" ^ message)) val messages' = (urgent, (tool, message')) :: messages val store' = (tool, message') :: (if length store <= message_store_limit then store - else #1 (chop message_store_limit store)); + else #1 (chop message_store_limit store)) in make_state manager timeout_heap active' canceling' messages' store' end - | NONE => state)); + | NONE => state)) (* main manager thread -- only one may exist *) -val min_wait_time = seconds 0.3; -val max_wait_time = seconds 10.0; +val min_wait_time = seconds 0.3 +val max_wait_time = seconds 10.0 fun replace_all bef aft = let @@ -119,7 +118,8 @@ postponed_messages store)) |> map (fn (_, (tool, (worker, work))) => ((tool, work), worker)) |> AList.group (op =) - |> List.app (fn ((tool, work), workers) => + |> List.app (fn ((_, ""), _) => () + | ((tool, work), workers) => tool ^ ": " ^ implode_message (workers |> sort_distinct string_ord, work) |> break_into_chunks @@ -133,12 +133,12 @@ fun time_limit timeout_heap = (case try Thread_Heap.min timeout_heap of NONE => Time.+ (Time.now (), max_wait_time) - | SOME (time, _) => time); + | SOME (time, _) => time) (*action: find threads whose timeout is reached, and interrupt canceling threads*) fun action {manager, timeout_heap, active, canceling, messages, store} = let val (timeout_threads, timeout_heap') = - Thread_Heap.upto (Time.now (), Thread.self ()) timeout_heap; + Thread_Heap.upto (Time.now (), Thread.self ()) timeout_heap in if null timeout_threads andalso null canceling then NONE @@ -146,9 +146,9 @@ let val _ = List.app (Simple_Thread.interrupt_unsynchronized o #1) canceling val canceling' = filter (Thread.isActive o #1) canceling - val state' = make_state manager timeout_heap' active canceling' messages store; + val state' = make_state manager timeout_heap' active canceling' messages store in SOME (map #2 timeout_threads, state') end - end; + end in while Synchronized.change_result global_state (fn state as {timeout_heap, active, canceling, messages, store, ...} => @@ -156,12 +156,13 @@ then (false, make_state NONE timeout_heap active canceling messages store) else (true, state)) do - (Synchronized.timed_access global_state (SOME o time_limit o #timeout_heap) action - |> these - |> List.app (unregister (false, "Timed out.")); - print_new_messages (); - (*give threads some time to respond to interrupt*) - OS.Process.sleep min_wait_time) + (Synchronized.timed_access global_state + (SOME o time_limit o #timeout_heap) action + |> these + |> List.app (unregister (false, "Timed out.")); + print_new_messages (); + (* give threads some time to respond to interrupt *) + OS.Process.sleep min_wait_time) end)) in make_state manager timeout_heap active canceling messages store end) @@ -172,9 +173,9 @@ (Synchronized.change global_state (fn {manager, timeout_heap, active, canceling, messages, store} => let - val timeout_heap' = Thread_Heap.insert (death_time, thread) timeout_heap; - val active' = update_thread (thread, (tool, birth_time, death_time, desc)) active; - val state' = make_state manager timeout_heap' active' canceling messages store; + val timeout_heap' = Thread_Heap.insert (death_time, thread) timeout_heap + val active' = update_thread (thread, (tool, birth_time, death_time, desc)) active + val state' = make_state manager timeout_heap' active' canceling messages store in state' end); check_thread_manager ()) @@ -200,33 +201,36 @@ map_filter (fn (th, (tool', _, _, desc)) => if tool' = tool then SOME (th, (tool', Time.now (), desc)) else NONE) active - val state' = make_state manager timeout_heap [] (killing @ canceling) messages store; + val state' = make_state manager timeout_heap [] (killing @ canceling) messages store val _ = if null killing then () else Output.urgent_message ("Interrupted active " ^ das_wort_worker ^ "s.") - in state' end); + in state' end) (* running threads *) fun seconds time = string_of_int (Time.toSeconds time) ^ " s" +fun has_running_threads tool = + exists (fn (_, (tool', _, _, _)) => tool' = tool) + (#active (Synchronized.value global_state)) + fun running_threads tool das_wort_worker = let - val {active, canceling, ...} = Synchronized.value global_state; - - val now = Time.now (); + val {active, canceling, ...} = Synchronized.value global_state + val now = Time.now () fun running_info (_, (tool', birth_time, death_time, desc)) = if tool' = tool then SOME ("Running: " ^ seconds (Time.- (now, birth_time)) ^ " -- " ^ seconds (Time.- (death_time, now)) ^ " to live:\n" ^ - implode_desc desc) + op ^ desc) else NONE fun canceling_info (_, (tool', death_time, desc)) = if tool' = tool then SOME ("Trying to interrupt " ^ das_wort_worker ^ " since " ^ - seconds (Time.- (now, death_time)) ^ ":\n" ^ implode_desc desc) + seconds (Time.- (now, death_time)) ^ ":\n" ^ op ^ desc) else NONE val running = @@ -241,14 +245,14 @@ fun thread_messages tool das_wort_worker opt_limit = let - val limit = the_default message_display_limit opt_limit; + val limit = the_default message_display_limit opt_limit val tool_store = Synchronized.value global_state |> #store |> filter (curry (op =) tool o fst) val header = "Recent " ^ das_wort_worker ^ " messages" ^ (if length tool_store <= limit then ":" - else " (" ^ string_of_int limit ^ " displayed):"); - val ss = tool_store |> chop limit |> #1 |> map (implode_desc o snd) + else " (" ^ string_of_int limit ^ " displayed):") + val ss = tool_store |> chop limit |> #1 |> map (op ^ o snd) in List.app Output.urgent_message (header :: maps break_into_chunks ss) end end;