--- a/src/HOL/Tools/ATP/async_manager.ML Tue Aug 31 23:50:59 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,241 +0,0 @@
-(* Title: HOL/Tools/ATP/async_manager.ML
- Author: Fabian Immler, TU Muenchen
- Author: Makarius
- Author: Jasmin Blanchette, TU Muenchen
-
-Central manager for asynchronous diagnosis tool threads.
-*)
-
-signature ASYNC_MANAGER =
-sig
- val launch :
- string -> bool -> Time.time -> Time.time -> string -> (unit -> string)
- -> unit
- val kill_threads : string -> string -> unit
- val running_threads : string -> string -> unit
- val thread_messages : string -> string -> int option -> unit
-end;
-
-structure Async_Manager : ASYNC_MANAGER =
-struct
-
-(** preferences **)
-
-val message_store_limit = 20;
-val message_display_limit = 5;
-
-
-(** thread management **)
-
-(* data structures over threads *)
-
-structure Thread_Heap = Heap
-(
- 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;
-
-
-(* state of thread manager *)
-
-type state =
- {manager: Thread.thread option,
- timeout_heap: Thread_Heap.T,
- active: (Thread.thread * (string * Time.time * Time.time * string)) list,
- canceling: (Thread.thread * (string * Time.time * string)) list,
- messages: (string * string) list,
- store: (string * string) list}
-
-fun make_state manager timeout_heap active canceling messages store : state =
- {manager = manager, timeout_heap = timeout_heap, active = active,
- canceling = canceling, messages = messages, store = store}
-
-val global_state = Synchronized.var "async_manager"
- (make_state NONE Thread_Heap.empty [] [] [] []);
-
-
-(* unregister thread *)
-
-fun unregister verbose message thread =
- Synchronized.change global_state
- (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
- (case lookup_thread active thread of
- SOME (tool, birth_time, _, desc) =>
- let
- val active' = delete_thread thread active;
- val now = Time.now ()
- val canceling' = (thread, (tool, now, desc)) :: canceling
- val message' =
- desc ^ "\n" ^ message ^
- (if verbose then
- "\nTotal time: " ^ Int.toString (Time.toMilliseconds
- (Time.- (now, birth_time))) ^ " ms."
- else
- "")
- val messages' = (tool, message') :: messages;
- val store' = (tool, message') ::
- (if length store <= message_store_limit then store
- else #1 (chop message_store_limit store));
- in make_state manager timeout_heap active' canceling' messages' store' end
- | NONE => state));
-
-
-(* main manager thread -- only one may exist *)
-
-val min_wait_time = Time.fromMilliseconds 300;
-val max_wait_time = Time.fromSeconds 10;
-
-fun replace_all bef aft =
- let
- fun aux seen "" = String.implode (rev seen)
- | aux seen s =
- if String.isPrefix bef s then
- aux seen "" ^ aft ^ aux [] (unprefix bef s)
- else
- aux (String.sub (s, 0) :: seen) (String.extract (s, 1, NONE))
- in aux [] end
-
-(* 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
-
-fun print_new_messages () =
- case Synchronized.change_result global_state
- (fn {manager, timeout_heap, active, canceling, messages, store} =>
- (messages, make_state manager timeout_heap active canceling []
- store)) of
- [] => ()
- | msgs as (tool, _) :: _ =>
- let val ss = break_into_chunks msgs in
- List.app priority (tool ^ ": " ^ hd ss :: tl ss)
- end
-
-fun check_thread_manager verbose = Synchronized.change global_state
- (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
- if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state
- else let val manager = SOME (Toplevel.thread false (fn () =>
- let
- fun time_limit timeout_heap =
- (case try Thread_Heap.min timeout_heap of
- NONE => Time.+ (Time.now (), max_wait_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;
- in
- if null timeout_threads andalso null canceling then
- NONE
- else
- let
- val _ = List.app (Simple_Thread.interrupt o #1) canceling
- val canceling' = filter (Thread.isActive o #1) canceling
- val state' = make_state manager timeout_heap' active canceling' messages store;
- in SOME (map #2 timeout_threads, state') end
- end;
- in
- while Synchronized.change_result global_state
- (fn state as {timeout_heap, active, canceling, messages, store, ...} =>
- if null active andalso null canceling andalso null messages
- 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 verbose "Timed out.\n");
- 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)
-
-
-(* register thread *)
-
-fun register tool verbose birth_time death_time desc thread =
- (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;
- in state' end);
- check_thread_manager verbose);
-
-
-fun launch tool verbose birth_time death_time desc f =
- (Toplevel.thread true
- (fn () =>
- let
- val self = Thread.self ()
- val _ = register tool verbose birth_time death_time desc self
- val message = f ()
- in unregister verbose message self end);
- ())
-
-
-(** user commands **)
-
-(* kill threads *)
-
-fun kill_threads tool workers = Synchronized.change global_state
- (fn {manager, timeout_heap, active, canceling, messages, store} =>
- let
- val killing =
- 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 _ = if null killing then () else priority ("Killed active " ^ workers ^ ".")
- in state' end);
-
-
-(* running threads *)
-
-fun seconds time = string_of_int (Time.toSeconds time) ^ " s"
-
-fun running_threads tool workers =
- let
- 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" ^ desc)
- else
- NONE
- fun canceling_info (_, (tool', death_time, desc)) =
- if tool' = tool then
- SOME ("Trying to interrupt thread since " ^
- seconds (Time.- (now, death_time)) ^ ":\n" ^ desc)
- else
- NONE
- val running =
- case map_filter running_info active of
- [] => ["No " ^ workers ^ " running."]
- | ss => "Running " ^ workers ^ ":" :: ss
- val interrupting =
- case map_filter canceling_info canceling of
- [] => []
- | ss => "Trying to interrupt the following " ^ workers ^ ":" :: ss
- in priority (space_implode "\n\n" (running @ interrupting)) end
-
-fun thread_messages tool worker opt_limit =
- let
- 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 " ^ 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
-
-end;