load "try" after "Metis" and move "Async_Manager" back to Sledgehammer
authorblanchet
Tue Dec 07 09:58:56 2010 +0100 (2010-12-07)
changeset 410428275f52ac991
parent 41041 ec2734f34d0f
child 41044 1c0eefa8d02a
child 41045 2a41709f34c1
load "try" after "Metis" and move "Async_Manager" back to Sledgehammer
src/HOL/HOL.thy
src/HOL/IsaMakefile
src/HOL/Metis.thy
src/HOL/Sledgehammer.thy
src/HOL/Tools/Sledgehammer/async_manager.ML
src/HOL/Tools/async_manager.ML
     1.1 --- a/src/HOL/HOL.thy	Tue Dec 07 09:58:52 2010 +0100
     1.2 +++ b/src/HOL/HOL.thy	Tue Dec 07 09:58:56 2010 +0100
     1.3 @@ -29,8 +29,6 @@
     1.4    "~~/src/Tools/induct.ML"
     1.5    ("~~/src/Tools/induct_tacs.ML")
     1.6    ("Tools/recfun_codegen.ML")
     1.7 -  "Tools/async_manager.ML"
     1.8 -  "Tools/try.ML"
     1.9    ("Tools/cnf_funcs.ML")
    1.10    "~~/src/Tools/subtyping.ML"
    1.11  begin
    1.12 @@ -1982,10 +1980,6 @@
    1.13  *} "solve goal by normalization"
    1.14  
    1.15  
    1.16 -subsection {* Try *}
    1.17 -
    1.18 -setup {* Try.setup *}
    1.19 -
    1.20  subsection {* Counterexample Search Units *}
    1.21  
    1.22  subsubsection {* Quickcheck *}
     2.1 --- a/src/HOL/IsaMakefile	Tue Dec 07 09:58:52 2010 +0100
     2.2 +++ b/src/HOL/IsaMakefile	Tue Dec 07 09:58:56 2010 +0100
     2.3 @@ -224,7 +224,6 @@
     2.4    Tools/Metis/metis_translate.ML \
     2.5    Tools/abel_cancel.ML \
     2.6    Tools/arith_data.ML \
     2.7 -  Tools/async_manager.ML \
     2.8    Tools/cnf_funcs.ML \
     2.9    Tools/dseq.ML \
    2.10    Tools/inductive.ML \
    2.11 @@ -344,6 +343,7 @@
    2.12    Tools/recdef.ML \
    2.13    Tools/record.ML \
    2.14    Tools/semiring_normalizer.ML \
    2.15 +  Tools/Sledgehammer/async_manager.ML \
    2.16    Tools/Sledgehammer/sledgehammer.ML \
    2.17    Tools/Sledgehammer/sledgehammer_filter.ML \
    2.18    Tools/Sledgehammer/sledgehammer_minimize.ML \
     3.1 --- a/src/HOL/Metis.thy	Tue Dec 07 09:58:52 2010 +0100
     3.2 +++ b/src/HOL/Metis.thy	Tue Dec 07 09:58:56 2010 +0100
     3.3 @@ -12,6 +12,7 @@
     3.4       ("Tools/Metis/metis_translate.ML")
     3.5       ("Tools/Metis/metis_reconstruct.ML")
     3.6       ("Tools/Metis/metis_tactics.ML")
     3.7 +     ("Tools/try.ML")
     3.8  begin
     3.9  
    3.10  definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
    3.11 @@ -38,4 +39,10 @@
    3.12  hide_const (open) fequal
    3.13  hide_fact (open) fequal_def fequal_imp_equal equal_imp_fequal equal_imp_equal
    3.14  
    3.15 +subsection {* Try *}
    3.16 +
    3.17 +use "Tools/try.ML"
    3.18 +
    3.19 +setup {* Try.setup *}
    3.20 +
    3.21  end
     4.1 --- a/src/HOL/Sledgehammer.thy	Tue Dec 07 09:58:52 2010 +0100
     4.2 +++ b/src/HOL/Sledgehammer.thy	Tue Dec 07 09:58:56 2010 +0100
     4.3 @@ -8,7 +8,8 @@
     4.4  
     4.5  theory Sledgehammer
     4.6  imports ATP SMT
     4.7 -uses "Tools/Sledgehammer/sledgehammer_util.ML"
     4.8 +uses "Tools/Sledgehammer/async_manager.ML"
     4.9 +     "Tools/Sledgehammer/sledgehammer_util.ML"
    4.10       "Tools/Sledgehammer/sledgehammer_filter.ML"
    4.11       "Tools/Sledgehammer/sledgehammer_atp_translate.ML"
    4.12       "Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML"
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Tools/Sledgehammer/async_manager.ML	Tue Dec 07 09:58:56 2010 +0100
     5.3 @@ -0,0 +1,237 @@
     5.4 +(*  Title:      HOL/Tools/Sledgehammer/async_manager.ML
     5.5 +    Author:     Fabian Immler, TU Muenchen
     5.6 +    Author:     Makarius
     5.7 +    Author:     Jasmin Blanchette, TU Muenchen
     5.8 +
     5.9 +Central manager for asynchronous diagnosis tool threads.
    5.10 +*)
    5.11 +
    5.12 +signature ASYNC_MANAGER =
    5.13 +sig
    5.14 +  val break_into_chunks : string list -> string list
    5.15 +  val launch :
    5.16 +    string -> Time.time -> Time.time -> string -> (unit -> string) -> unit
    5.17 +  val kill_threads : string -> string -> unit
    5.18 +  val running_threads : string -> string -> unit
    5.19 +  val thread_messages : string -> string -> int option -> unit
    5.20 +end;
    5.21 +
    5.22 +structure Async_Manager : ASYNC_MANAGER =
    5.23 +struct
    5.24 +
    5.25 +(** preferences **)
    5.26 +
    5.27 +val message_store_limit = 20;
    5.28 +val message_display_limit = 5;
    5.29 +
    5.30 +
    5.31 +(** thread management **)
    5.32 +
    5.33 +(* data structures over threads *)
    5.34 +
    5.35 +structure Thread_Heap = Heap
    5.36 +(
    5.37 +  type elem = Time.time * Thread.thread;
    5.38 +  fun ord ((a, _), (b, _)) = Time.compare (a, b);
    5.39 +);
    5.40 +
    5.41 +fun lookup_thread xs = AList.lookup Thread.equal xs;
    5.42 +fun delete_thread xs = AList.delete Thread.equal xs;
    5.43 +fun update_thread xs = AList.update Thread.equal xs;
    5.44 +
    5.45 +
    5.46 +(* state of thread manager *)
    5.47 +
    5.48 +type state =
    5.49 +  {manager: Thread.thread option,
    5.50 +   timeout_heap: Thread_Heap.T,
    5.51 +   active: (Thread.thread * (string * Time.time * Time.time * string)) list,
    5.52 +   canceling: (Thread.thread * (string * Time.time * string)) list,
    5.53 +   messages: (string * string) list,
    5.54 +   store: (string * string) list}
    5.55 +
    5.56 +fun make_state manager timeout_heap active canceling messages store : state =
    5.57 +  {manager = manager, timeout_heap = timeout_heap, active = active,
    5.58 +   canceling = canceling, messages = messages, store = store}
    5.59 +
    5.60 +val global_state = Synchronized.var "async_manager"
    5.61 +  (make_state NONE Thread_Heap.empty [] [] [] []);
    5.62 +
    5.63 +
    5.64 +(* unregister thread *)
    5.65 +
    5.66 +fun unregister message thread =
    5.67 +  Synchronized.change global_state
    5.68 +  (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
    5.69 +    (case lookup_thread active thread of
    5.70 +      SOME (tool, _, _, desc) =>
    5.71 +        let
    5.72 +          val active' = delete_thread thread active;
    5.73 +          val now = Time.now ()
    5.74 +          val canceling' = (thread, (tool, now, desc)) :: canceling
    5.75 +          val message' = desc ^ "\n" ^ message
    5.76 +          val messages' = (tool, message') :: messages;
    5.77 +          val store' = (tool, message') ::
    5.78 +            (if length store <= message_store_limit then store
    5.79 +             else #1 (chop message_store_limit store));
    5.80 +        in make_state manager timeout_heap active' canceling' messages' store' end
    5.81 +    | NONE => state));
    5.82 +
    5.83 +
    5.84 +(* main manager thread -- only one may exist *)
    5.85 +
    5.86 +val min_wait_time = seconds 0.3;
    5.87 +val max_wait_time = seconds 10.0;
    5.88 +
    5.89 +fun replace_all bef aft =
    5.90 +  let
    5.91 +    fun aux seen "" = String.implode (rev seen)
    5.92 +      | aux seen s =
    5.93 +        if String.isPrefix bef s then
    5.94 +          aux seen "" ^ aft ^ aux [] (unprefix bef s)
    5.95 +        else
    5.96 +          aux (String.sub (s, 0) :: seen) (String.extract (s, 1, NONE))
    5.97 +  in aux [] end
    5.98 +
    5.99 +(* This is a workaround for Proof General's off-by-a-few sendback display bug,
   5.100 +   whereby "pr" in "proof" is not highlighted. *)
   5.101 +val break_into_chunks = maps (space_explode "\000" o replace_all "\n\n" "\000")
   5.102 +
   5.103 +fun print_new_messages () =
   5.104 +  case Synchronized.change_result global_state
   5.105 +         (fn {manager, timeout_heap, active, canceling, messages, store} =>
   5.106 +             (messages, make_state manager timeout_heap active canceling []
   5.107 +                                   store)) of
   5.108 +    [] => ()
   5.109 +  | msgs as (tool, _) :: _ =>
   5.110 +    let val ss = break_into_chunks (map snd msgs) in
   5.111 +      List.app Output.urgent_message (tool ^ ": " ^ hd ss :: tl ss)
   5.112 +    end
   5.113 +
   5.114 +fun check_thread_manager () = Synchronized.change global_state
   5.115 +  (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
   5.116 +    if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state
   5.117 +    else let val manager = SOME (Toplevel.thread false (fn () =>
   5.118 +      let
   5.119 +        fun time_limit timeout_heap =
   5.120 +          (case try Thread_Heap.min timeout_heap of
   5.121 +            NONE => Time.+ (Time.now (), max_wait_time)
   5.122 +          | SOME (time, _) => time);
   5.123 +
   5.124 +        (*action: find threads whose timeout is reached, and interrupt canceling threads*)
   5.125 +        fun action {manager, timeout_heap, active, canceling, messages, store} =
   5.126 +          let val (timeout_threads, timeout_heap') =
   5.127 +            Thread_Heap.upto (Time.now (), Thread.self ()) timeout_heap;
   5.128 +          in
   5.129 +            if null timeout_threads andalso null canceling then
   5.130 +              NONE
   5.131 +            else
   5.132 +              let
   5.133 +                val _ = List.app (Simple_Thread.interrupt o #1) canceling
   5.134 +                val canceling' = filter (Thread.isActive o #1) canceling
   5.135 +                val state' = make_state manager timeout_heap' active canceling' messages store;
   5.136 +              in SOME (map #2 timeout_threads, state') end
   5.137 +          end;
   5.138 +      in
   5.139 +        while Synchronized.change_result global_state
   5.140 +          (fn state as {timeout_heap, active, canceling, messages, store, ...} =>
   5.141 +            if null active andalso null canceling andalso null messages
   5.142 +            then (false, make_state NONE timeout_heap active canceling messages store)
   5.143 +            else (true, state))
   5.144 +        do
   5.145 +          (Synchronized.timed_access global_state (SOME o time_limit o #timeout_heap) action
   5.146 +            |> these
   5.147 +            |> List.app (unregister "Timed out.\n");
   5.148 +            print_new_messages ();
   5.149 +            (*give threads some time to respond to interrupt*)
   5.150 +            OS.Process.sleep min_wait_time)
   5.151 +      end))
   5.152 +    in make_state manager timeout_heap active canceling messages store end)
   5.153 +
   5.154 +
   5.155 +(* register thread *)
   5.156 +
   5.157 +fun register tool birth_time death_time desc thread =
   5.158 + (Synchronized.change global_state
   5.159 +    (fn {manager, timeout_heap, active, canceling, messages, store} =>
   5.160 +      let
   5.161 +        val timeout_heap' = Thread_Heap.insert (death_time, thread) timeout_heap;
   5.162 +        val active' = update_thread (thread, (tool, birth_time, death_time, desc)) active;
   5.163 +        val state' = make_state manager timeout_heap' active' canceling messages store;
   5.164 +      in state' end);
   5.165 +  check_thread_manager ())
   5.166 +
   5.167 +
   5.168 +fun launch tool birth_time death_time desc f =
   5.169 +  (Toplevel.thread true
   5.170 +       (fn () =>
   5.171 +           let
   5.172 +             val self = Thread.self ()
   5.173 +             val _ = register tool birth_time death_time desc self
   5.174 +             val message = f ()
   5.175 +           in unregister message self end);
   5.176 +   ())
   5.177 +
   5.178 +
   5.179 +(** user commands **)
   5.180 +
   5.181 +(* kill threads *)
   5.182 +
   5.183 +fun kill_threads tool workers = Synchronized.change global_state
   5.184 +  (fn {manager, timeout_heap, active, canceling, messages, store} =>
   5.185 +    let
   5.186 +      val killing =
   5.187 +        map_filter (fn (th, (tool', _, _, desc)) =>
   5.188 +                       if tool' = tool then SOME (th, (tool', Time.now (), desc))
   5.189 +                       else NONE) active
   5.190 +      val state' = make_state manager timeout_heap [] (killing @ canceling) messages store;
   5.191 +      val _ = if null killing then () else Output.urgent_message ("Killed active " ^ workers ^ ".")
   5.192 +    in state' end);
   5.193 +
   5.194 +
   5.195 +(* running threads *)
   5.196 +
   5.197 +fun seconds time = string_of_int (Time.toSeconds time) ^ " s"
   5.198 +
   5.199 +fun running_threads tool workers =
   5.200 +  let
   5.201 +    val {active, canceling, ...} = Synchronized.value global_state;
   5.202 +
   5.203 +    val now = Time.now ();
   5.204 +    fun running_info (_, (tool', birth_time, death_time, desc)) =
   5.205 +      if tool' = tool then
   5.206 +        SOME ("Running: " ^ seconds (Time.- (now, birth_time)) ^ " -- " ^
   5.207 +              seconds (Time.- (death_time, now)) ^ " to live:\n" ^ desc)
   5.208 +      else
   5.209 +        NONE
   5.210 +    fun canceling_info (_, (tool', death_time, desc)) =
   5.211 +      if tool' = tool then
   5.212 +        SOME ("Trying to interrupt thread since " ^
   5.213 +              seconds (Time.- (now, death_time)) ^ ":\n" ^ desc)
   5.214 +      else
   5.215 +        NONE
   5.216 +    val running =
   5.217 +      case map_filter running_info active of
   5.218 +        [] => ["No " ^ workers ^ " running."]
   5.219 +      | ss => "Running " ^ workers ^ ":" :: ss
   5.220 +    val interrupting =
   5.221 +      case map_filter canceling_info canceling of
   5.222 +        [] => []
   5.223 +      | ss => "Trying to interrupt the following " ^ workers ^ ":" :: ss
   5.224 +  in Output.urgent_message (space_implode "\n\n" (running @ interrupting)) end
   5.225 +
   5.226 +fun thread_messages tool worker opt_limit =
   5.227 +  let
   5.228 +    val limit = the_default message_display_limit opt_limit;
   5.229 +    val tool_store = Synchronized.value global_state
   5.230 +                     |> #store |> filter (curry (op =) tool o fst)
   5.231 +    val header =
   5.232 +      "Recent " ^ worker ^ " messages" ^
   5.233 +        (if length tool_store <= limit then ":"
   5.234 +         else " (" ^ string_of_int limit ^ " displayed):");
   5.235 +  in
   5.236 +    List.app Output.urgent_message (header :: break_into_chunks
   5.237 +                                     (map snd (#1 (chop limit tool_store))))
   5.238 +  end
   5.239 +
   5.240 +end;
     6.1 --- a/src/HOL/Tools/async_manager.ML	Tue Dec 07 09:58:52 2010 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,237 +0,0 @@
     6.4 -(*  Title:      HOL/Tools/async_manager.ML
     6.5 -    Author:     Fabian Immler, TU Muenchen
     6.6 -    Author:     Makarius
     6.7 -    Author:     Jasmin Blanchette, TU Muenchen
     6.8 -
     6.9 -Central manager for asynchronous diagnosis tool threads.
    6.10 -*)
    6.11 -
    6.12 -signature ASYNC_MANAGER =
    6.13 -sig
    6.14 -  val break_into_chunks : string list -> string list
    6.15 -  val launch :
    6.16 -    string -> Time.time -> Time.time -> string -> (unit -> string) -> unit
    6.17 -  val kill_threads : string -> string -> unit
    6.18 -  val running_threads : string -> string -> unit
    6.19 -  val thread_messages : string -> string -> int option -> unit
    6.20 -end;
    6.21 -
    6.22 -structure Async_Manager : ASYNC_MANAGER =
    6.23 -struct
    6.24 -
    6.25 -(** preferences **)
    6.26 -
    6.27 -val message_store_limit = 20;
    6.28 -val message_display_limit = 5;
    6.29 -
    6.30 -
    6.31 -(** thread management **)
    6.32 -
    6.33 -(* data structures over threads *)
    6.34 -
    6.35 -structure Thread_Heap = Heap
    6.36 -(
    6.37 -  type elem = Time.time * Thread.thread;
    6.38 -  fun ord ((a, _), (b, _)) = Time.compare (a, b);
    6.39 -);
    6.40 -
    6.41 -fun lookup_thread xs = AList.lookup Thread.equal xs;
    6.42 -fun delete_thread xs = AList.delete Thread.equal xs;
    6.43 -fun update_thread xs = AList.update Thread.equal xs;
    6.44 -
    6.45 -
    6.46 -(* state of thread manager *)
    6.47 -
    6.48 -type state =
    6.49 -  {manager: Thread.thread option,
    6.50 -   timeout_heap: Thread_Heap.T,
    6.51 -   active: (Thread.thread * (string * Time.time * Time.time * string)) list,
    6.52 -   canceling: (Thread.thread * (string * Time.time * string)) list,
    6.53 -   messages: (string * string) list,
    6.54 -   store: (string * string) list}
    6.55 -
    6.56 -fun make_state manager timeout_heap active canceling messages store : state =
    6.57 -  {manager = manager, timeout_heap = timeout_heap, active = active,
    6.58 -   canceling = canceling, messages = messages, store = store}
    6.59 -
    6.60 -val global_state = Synchronized.var "async_manager"
    6.61 -  (make_state NONE Thread_Heap.empty [] [] [] []);
    6.62 -
    6.63 -
    6.64 -(* unregister thread *)
    6.65 -
    6.66 -fun unregister message thread =
    6.67 -  Synchronized.change global_state
    6.68 -  (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
    6.69 -    (case lookup_thread active thread of
    6.70 -      SOME (tool, _, _, desc) =>
    6.71 -        let
    6.72 -          val active' = delete_thread thread active;
    6.73 -          val now = Time.now ()
    6.74 -          val canceling' = (thread, (tool, now, desc)) :: canceling
    6.75 -          val message' = desc ^ "\n" ^ message
    6.76 -          val messages' = (tool, message') :: messages;
    6.77 -          val store' = (tool, message') ::
    6.78 -            (if length store <= message_store_limit then store
    6.79 -             else #1 (chop message_store_limit store));
    6.80 -        in make_state manager timeout_heap active' canceling' messages' store' end
    6.81 -    | NONE => state));
    6.82 -
    6.83 -
    6.84 -(* main manager thread -- only one may exist *)
    6.85 -
    6.86 -val min_wait_time = seconds 0.3;
    6.87 -val max_wait_time = seconds 10.0;
    6.88 -
    6.89 -fun replace_all bef aft =
    6.90 -  let
    6.91 -    fun aux seen "" = String.implode (rev seen)
    6.92 -      | aux seen s =
    6.93 -        if String.isPrefix bef s then
    6.94 -          aux seen "" ^ aft ^ aux [] (unprefix bef s)
    6.95 -        else
    6.96 -          aux (String.sub (s, 0) :: seen) (String.extract (s, 1, NONE))
    6.97 -  in aux [] end
    6.98 -
    6.99 -(* This is a workaround for Proof General's off-by-a-few sendback display bug,
   6.100 -   whereby "pr" in "proof" is not highlighted. *)
   6.101 -val break_into_chunks = maps (space_explode "\000" o replace_all "\n\n" "\000")
   6.102 -
   6.103 -fun print_new_messages () =
   6.104 -  case Synchronized.change_result global_state
   6.105 -         (fn {manager, timeout_heap, active, canceling, messages, store} =>
   6.106 -             (messages, make_state manager timeout_heap active canceling []
   6.107 -                                   store)) of
   6.108 -    [] => ()
   6.109 -  | msgs as (tool, _) :: _ =>
   6.110 -    let val ss = break_into_chunks (map snd msgs) in
   6.111 -      List.app Output.urgent_message (tool ^ ": " ^ hd ss :: tl ss)
   6.112 -    end
   6.113 -
   6.114 -fun check_thread_manager () = Synchronized.change global_state
   6.115 -  (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
   6.116 -    if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state
   6.117 -    else let val manager = SOME (Toplevel.thread false (fn () =>
   6.118 -      let
   6.119 -        fun time_limit timeout_heap =
   6.120 -          (case try Thread_Heap.min timeout_heap of
   6.121 -            NONE => Time.+ (Time.now (), max_wait_time)
   6.122 -          | SOME (time, _) => time);
   6.123 -
   6.124 -        (*action: find threads whose timeout is reached, and interrupt canceling threads*)
   6.125 -        fun action {manager, timeout_heap, active, canceling, messages, store} =
   6.126 -          let val (timeout_threads, timeout_heap') =
   6.127 -            Thread_Heap.upto (Time.now (), Thread.self ()) timeout_heap;
   6.128 -          in
   6.129 -            if null timeout_threads andalso null canceling then
   6.130 -              NONE
   6.131 -            else
   6.132 -              let
   6.133 -                val _ = List.app (Simple_Thread.interrupt o #1) canceling
   6.134 -                val canceling' = filter (Thread.isActive o #1) canceling
   6.135 -                val state' = make_state manager timeout_heap' active canceling' messages store;
   6.136 -              in SOME (map #2 timeout_threads, state') end
   6.137 -          end;
   6.138 -      in
   6.139 -        while Synchronized.change_result global_state
   6.140 -          (fn state as {timeout_heap, active, canceling, messages, store, ...} =>
   6.141 -            if null active andalso null canceling andalso null messages
   6.142 -            then (false, make_state NONE timeout_heap active canceling messages store)
   6.143 -            else (true, state))
   6.144 -        do
   6.145 -          (Synchronized.timed_access global_state (SOME o time_limit o #timeout_heap) action
   6.146 -            |> these
   6.147 -            |> List.app (unregister "Timed out.\n");
   6.148 -            print_new_messages ();
   6.149 -            (*give threads some time to respond to interrupt*)
   6.150 -            OS.Process.sleep min_wait_time)
   6.151 -      end))
   6.152 -    in make_state manager timeout_heap active canceling messages store end)
   6.153 -
   6.154 -
   6.155 -(* register thread *)
   6.156 -
   6.157 -fun register tool birth_time death_time desc thread =
   6.158 - (Synchronized.change global_state
   6.159 -    (fn {manager, timeout_heap, active, canceling, messages, store} =>
   6.160 -      let
   6.161 -        val timeout_heap' = Thread_Heap.insert (death_time, thread) timeout_heap;
   6.162 -        val active' = update_thread (thread, (tool, birth_time, death_time, desc)) active;
   6.163 -        val state' = make_state manager timeout_heap' active' canceling messages store;
   6.164 -      in state' end);
   6.165 -  check_thread_manager ())
   6.166 -
   6.167 -
   6.168 -fun launch tool birth_time death_time desc f =
   6.169 -  (Toplevel.thread true
   6.170 -       (fn () =>
   6.171 -           let
   6.172 -             val self = Thread.self ()
   6.173 -             val _ = register tool birth_time death_time desc self
   6.174 -             val message = f ()
   6.175 -           in unregister message self end);
   6.176 -   ())
   6.177 -
   6.178 -
   6.179 -(** user commands **)
   6.180 -
   6.181 -(* kill threads *)
   6.182 -
   6.183 -fun kill_threads tool workers = Synchronized.change global_state
   6.184 -  (fn {manager, timeout_heap, active, canceling, messages, store} =>
   6.185 -    let
   6.186 -      val killing =
   6.187 -        map_filter (fn (th, (tool', _, _, desc)) =>
   6.188 -                       if tool' = tool then SOME (th, (tool', Time.now (), desc))
   6.189 -                       else NONE) active
   6.190 -      val state' = make_state manager timeout_heap [] (killing @ canceling) messages store;
   6.191 -      val _ = if null killing then () else Output.urgent_message ("Killed active " ^ workers ^ ".")
   6.192 -    in state' end);
   6.193 -
   6.194 -
   6.195 -(* running threads *)
   6.196 -
   6.197 -fun seconds time = string_of_int (Time.toSeconds time) ^ " s"
   6.198 -
   6.199 -fun running_threads tool workers =
   6.200 -  let
   6.201 -    val {active, canceling, ...} = Synchronized.value global_state;
   6.202 -
   6.203 -    val now = Time.now ();
   6.204 -    fun running_info (_, (tool', birth_time, death_time, desc)) =
   6.205 -      if tool' = tool then
   6.206 -        SOME ("Running: " ^ seconds (Time.- (now, birth_time)) ^ " -- " ^
   6.207 -              seconds (Time.- (death_time, now)) ^ " to live:\n" ^ desc)
   6.208 -      else
   6.209 -        NONE
   6.210 -    fun canceling_info (_, (tool', death_time, desc)) =
   6.211 -      if tool' = tool then
   6.212 -        SOME ("Trying to interrupt thread since " ^
   6.213 -              seconds (Time.- (now, death_time)) ^ ":\n" ^ desc)
   6.214 -      else
   6.215 -        NONE
   6.216 -    val running =
   6.217 -      case map_filter running_info active of
   6.218 -        [] => ["No " ^ workers ^ " running."]
   6.219 -      | ss => "Running " ^ workers ^ ":" :: ss
   6.220 -    val interrupting =
   6.221 -      case map_filter canceling_info canceling of
   6.222 -        [] => []
   6.223 -      | ss => "Trying to interrupt the following " ^ workers ^ ":" :: ss
   6.224 -  in Output.urgent_message (space_implode "\n\n" (running @ interrupting)) end
   6.225 -
   6.226 -fun thread_messages tool worker opt_limit =
   6.227 -  let
   6.228 -    val limit = the_default message_display_limit opt_limit;
   6.229 -    val tool_store = Synchronized.value global_state
   6.230 -                     |> #store |> filter (curry (op =) tool o fst)
   6.231 -    val header =
   6.232 -      "Recent " ^ worker ^ " messages" ^
   6.233 -        (if length tool_store <= limit then ":"
   6.234 -         else " (" ^ string_of_int limit ^ " displayed):");
   6.235 -  in
   6.236 -    List.app Output.urgent_message (header :: break_into_chunks
   6.237 -                                     (map snd (#1 (chop limit tool_store))))
   6.238 -  end
   6.239 -
   6.240 -end;