move file
authorblanchet
Tue Aug 31 23:52:59 2010 +0200 (2010-08-31)
changeset 38989e34b099e477e
parent 38988 483879af0643
child 38990 7fba3ccc755a
move file
src/HOL/IsaMakefile
src/HOL/Tools/ATP/async_manager.ML
src/HOL/Tools/async_manager.ML
     1.1 --- a/src/HOL/IsaMakefile	Tue Aug 31 23:50:59 2010 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Tue Aug 31 23:52:59 2010 +0200
     1.3 @@ -266,7 +266,7 @@
     1.4    $(SRC)/Provers/Arith/combine_numerals.ML \
     1.5    $(SRC)/Provers/Arith/extract_common_term.ML \
     1.6    $(SRC)/Tools/Metis/metis.ML \
     1.7 -  Tools/ATP/async_manager.ML \
     1.8 +  Tools/async_manager.ML \
     1.9    Tools/ATP/atp_problem.ML \
    1.10    Tools/ATP/atp_systems.ML \
    1.11    Tools/choice_specification.ML \
     2.1 --- a/src/HOL/Tools/ATP/async_manager.ML	Tue Aug 31 23:50:59 2010 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,241 +0,0 @@
     2.4 -(*  Title:      HOL/Tools/ATP/async_manager.ML
     2.5 -    Author:     Fabian Immler, TU Muenchen
     2.6 -    Author:     Makarius
     2.7 -    Author:     Jasmin Blanchette, TU Muenchen
     2.8 -
     2.9 -Central manager for asynchronous diagnosis tool threads.
    2.10 -*)
    2.11 -
    2.12 -signature ASYNC_MANAGER =
    2.13 -sig
    2.14 -  val launch :
    2.15 -    string -> bool -> Time.time -> Time.time -> string -> (unit -> string)
    2.16 -    -> unit
    2.17 -  val kill_threads : string -> string -> unit
    2.18 -  val running_threads : string -> string -> unit
    2.19 -  val thread_messages : string -> string -> int option -> unit
    2.20 -end;
    2.21 -
    2.22 -structure Async_Manager : ASYNC_MANAGER =
    2.23 -struct
    2.24 -
    2.25 -(** preferences **)
    2.26 -
    2.27 -val message_store_limit = 20;
    2.28 -val message_display_limit = 5;
    2.29 -
    2.30 -
    2.31 -(** thread management **)
    2.32 -
    2.33 -(* data structures over threads *)
    2.34 -
    2.35 -structure Thread_Heap = Heap
    2.36 -(
    2.37 -  type elem = Time.time * Thread.thread;
    2.38 -  fun ord ((a, _), (b, _)) = Time.compare (a, b);
    2.39 -);
    2.40 -
    2.41 -fun lookup_thread xs = AList.lookup Thread.equal xs;
    2.42 -fun delete_thread xs = AList.delete Thread.equal xs;
    2.43 -fun update_thread xs = AList.update Thread.equal xs;
    2.44 -
    2.45 -
    2.46 -(* state of thread manager *)
    2.47 -
    2.48 -type state =
    2.49 -  {manager: Thread.thread option,
    2.50 -   timeout_heap: Thread_Heap.T,
    2.51 -   active: (Thread.thread * (string * Time.time * Time.time * string)) list,
    2.52 -   canceling: (Thread.thread * (string * Time.time * string)) list,
    2.53 -   messages: (string * string) list,
    2.54 -   store: (string * string) list}
    2.55 -
    2.56 -fun make_state manager timeout_heap active canceling messages store : state =
    2.57 -  {manager = manager, timeout_heap = timeout_heap, active = active,
    2.58 -   canceling = canceling, messages = messages, store = store}
    2.59 -
    2.60 -val global_state = Synchronized.var "async_manager"
    2.61 -  (make_state NONE Thread_Heap.empty [] [] [] []);
    2.62 -
    2.63 -
    2.64 -(* unregister thread *)
    2.65 -
    2.66 -fun unregister verbose message thread =
    2.67 -  Synchronized.change global_state
    2.68 -  (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
    2.69 -    (case lookup_thread active thread of
    2.70 -      SOME (tool, birth_time, _, desc) =>
    2.71 -        let
    2.72 -          val active' = delete_thread thread active;
    2.73 -          val now = Time.now ()
    2.74 -          val canceling' = (thread, (tool, now, desc)) :: canceling
    2.75 -          val message' =
    2.76 -            desc ^ "\n" ^ message ^
    2.77 -            (if verbose then
    2.78 -               "\nTotal time: " ^ Int.toString (Time.toMilliseconds
    2.79 -                                            (Time.- (now, birth_time))) ^ " ms."
    2.80 -             else
    2.81 -               "")
    2.82 -          val messages' = (tool, message') :: messages;
    2.83 -          val store' = (tool, message') ::
    2.84 -            (if length store <= message_store_limit then store
    2.85 -             else #1 (chop message_store_limit store));
    2.86 -        in make_state manager timeout_heap active' canceling' messages' store' end
    2.87 -    | NONE => state));
    2.88 -
    2.89 -
    2.90 -(* main manager thread -- only one may exist *)
    2.91 -
    2.92 -val min_wait_time = Time.fromMilliseconds 300;
    2.93 -val max_wait_time = Time.fromSeconds 10;
    2.94 -
    2.95 -fun replace_all bef aft =
    2.96 -  let
    2.97 -    fun aux seen "" = String.implode (rev seen)
    2.98 -      | aux seen s =
    2.99 -        if String.isPrefix bef s then
   2.100 -          aux seen "" ^ aft ^ aux [] (unprefix bef s)
   2.101 -        else
   2.102 -          aux (String.sub (s, 0) :: seen) (String.extract (s, 1, NONE))
   2.103 -  in aux [] end
   2.104 -
   2.105 -(* This is a workaround for Proof General's off-by-a-few sendback display bug,
   2.106 -   whereby "pr" in "proof" is not highlighted. *)
   2.107 -fun break_into_chunks xs =
   2.108 -  maps (space_explode "\000" o replace_all "\n\n" "\000" o snd) xs
   2.109 -
   2.110 -fun print_new_messages () =
   2.111 -  case Synchronized.change_result global_state
   2.112 -         (fn {manager, timeout_heap, active, canceling, messages, store} =>
   2.113 -             (messages, make_state manager timeout_heap active canceling []
   2.114 -                                   store)) of
   2.115 -    [] => ()
   2.116 -  | msgs as (tool, _) :: _ =>
   2.117 -    let val ss = break_into_chunks msgs in
   2.118 -      List.app priority (tool ^ ": " ^ hd ss :: tl ss)
   2.119 -    end
   2.120 -
   2.121 -fun check_thread_manager verbose = Synchronized.change global_state
   2.122 -  (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
   2.123 -    if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state
   2.124 -    else let val manager = SOME (Toplevel.thread false (fn () =>
   2.125 -      let
   2.126 -        fun time_limit timeout_heap =
   2.127 -          (case try Thread_Heap.min timeout_heap of
   2.128 -            NONE => Time.+ (Time.now (), max_wait_time)
   2.129 -          | SOME (time, _) => time);
   2.130 -
   2.131 -        (*action: find threads whose timeout is reached, and interrupt canceling threads*)
   2.132 -        fun action {manager, timeout_heap, active, canceling, messages, store} =
   2.133 -          let val (timeout_threads, timeout_heap') =
   2.134 -            Thread_Heap.upto (Time.now (), Thread.self ()) timeout_heap;
   2.135 -          in
   2.136 -            if null timeout_threads andalso null canceling then
   2.137 -              NONE
   2.138 -            else
   2.139 -              let
   2.140 -                val _ = List.app (Simple_Thread.interrupt o #1) canceling
   2.141 -                val canceling' = filter (Thread.isActive o #1) canceling
   2.142 -                val state' = make_state manager timeout_heap' active canceling' messages store;
   2.143 -              in SOME (map #2 timeout_threads, state') end
   2.144 -          end;
   2.145 -      in
   2.146 -        while Synchronized.change_result global_state
   2.147 -          (fn state as {timeout_heap, active, canceling, messages, store, ...} =>
   2.148 -            if null active andalso null canceling andalso null messages
   2.149 -            then (false, make_state NONE timeout_heap active canceling messages store)
   2.150 -            else (true, state))
   2.151 -        do
   2.152 -          (Synchronized.timed_access global_state (SOME o time_limit o #timeout_heap) action
   2.153 -            |> these
   2.154 -            |> List.app (unregister verbose "Timed out.\n");
   2.155 -            print_new_messages ();
   2.156 -            (*give threads some time to respond to interrupt*)
   2.157 -            OS.Process.sleep min_wait_time)
   2.158 -      end))
   2.159 -    in make_state manager timeout_heap active canceling messages store end)
   2.160 -
   2.161 -
   2.162 -(* register thread *)
   2.163 -
   2.164 -fun register tool verbose birth_time death_time desc thread =
   2.165 - (Synchronized.change global_state
   2.166 -    (fn {manager, timeout_heap, active, canceling, messages, store} =>
   2.167 -      let
   2.168 -        val timeout_heap' = Thread_Heap.insert (death_time, thread) timeout_heap;
   2.169 -        val active' = update_thread (thread, (tool, birth_time, death_time, desc)) active;
   2.170 -        val state' = make_state manager timeout_heap' active' canceling messages store;
   2.171 -      in state' end);
   2.172 -  check_thread_manager verbose);
   2.173 -
   2.174 -
   2.175 -fun launch tool verbose birth_time death_time desc f =
   2.176 -  (Toplevel.thread true
   2.177 -       (fn () =>
   2.178 -           let
   2.179 -             val self = Thread.self ()
   2.180 -             val _ = register tool verbose birth_time death_time desc self
   2.181 -             val message = f ()
   2.182 -           in unregister verbose message self end);
   2.183 -   ())
   2.184 -
   2.185 -
   2.186 -(** user commands **)
   2.187 -
   2.188 -(* kill threads *)
   2.189 -
   2.190 -fun kill_threads tool workers = Synchronized.change global_state
   2.191 -  (fn {manager, timeout_heap, active, canceling, messages, store} =>
   2.192 -    let
   2.193 -      val killing =
   2.194 -        map_filter (fn (th, (tool', _, _, desc)) =>
   2.195 -                       if tool' = tool then SOME (th, (tool', Time.now (), desc))
   2.196 -                       else NONE) active
   2.197 -      val state' = make_state manager timeout_heap [] (killing @ canceling) messages store;
   2.198 -      val _ = if null killing then () else priority ("Killed active " ^ workers ^ ".")
   2.199 -    in state' end);
   2.200 -
   2.201 -
   2.202 -(* running threads *)
   2.203 -
   2.204 -fun seconds time = string_of_int (Time.toSeconds time) ^ " s"
   2.205 -
   2.206 -fun running_threads tool workers =
   2.207 -  let
   2.208 -    val {active, canceling, ...} = Synchronized.value global_state;
   2.209 -
   2.210 -    val now = Time.now ();
   2.211 -    fun running_info (_, (tool', birth_time, death_time, desc)) =
   2.212 -      if tool' = tool then
   2.213 -        SOME ("Running: " ^ seconds (Time.- (now, birth_time)) ^ " -- " ^
   2.214 -              seconds (Time.- (death_time, now)) ^ " to live:\n" ^ desc)
   2.215 -      else
   2.216 -        NONE
   2.217 -    fun canceling_info (_, (tool', death_time, desc)) =
   2.218 -      if tool' = tool then
   2.219 -        SOME ("Trying to interrupt thread since " ^
   2.220 -              seconds (Time.- (now, death_time)) ^ ":\n" ^ desc)
   2.221 -      else
   2.222 -        NONE
   2.223 -    val running =
   2.224 -      case map_filter running_info active of
   2.225 -        [] => ["No " ^ workers ^ " running."]
   2.226 -      | ss => "Running " ^ workers ^ ":" :: ss
   2.227 -    val interrupting =
   2.228 -      case map_filter canceling_info canceling of
   2.229 -        [] => []
   2.230 -      | ss => "Trying to interrupt the following " ^ workers ^ ":" :: ss
   2.231 -  in priority (space_implode "\n\n" (running @ interrupting)) end
   2.232 -
   2.233 -fun thread_messages tool worker opt_limit =
   2.234 -  let
   2.235 -    val limit = the_default message_display_limit opt_limit;
   2.236 -    val tool_store = Synchronized.value global_state
   2.237 -                     |> #store |> filter (curry (op =) tool o fst)
   2.238 -    val header =
   2.239 -      "Recent " ^ worker ^ " messages" ^
   2.240 -        (if length tool_store <= limit then ":"
   2.241 -         else " (" ^ string_of_int limit ^ " displayed):");
   2.242 -  in List.app priority (header :: break_into_chunks (#1 (chop limit tool_store))) end
   2.243 -
   2.244 -end;
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Tools/async_manager.ML	Tue Aug 31 23:52:59 2010 +0200
     3.3 @@ -0,0 +1,241 @@
     3.4 +(*  Title:      HOL/Tools/ATP/async_manager.ML
     3.5 +    Author:     Fabian Immler, TU Muenchen
     3.6 +    Author:     Makarius
     3.7 +    Author:     Jasmin Blanchette, TU Muenchen
     3.8 +
     3.9 +Central manager for asynchronous diagnosis tool threads.
    3.10 +*)
    3.11 +
    3.12 +signature ASYNC_MANAGER =
    3.13 +sig
    3.14 +  val launch :
    3.15 +    string -> bool -> Time.time -> Time.time -> string -> (unit -> string)
    3.16 +    -> unit
    3.17 +  val kill_threads : string -> string -> unit
    3.18 +  val running_threads : string -> string -> unit
    3.19 +  val thread_messages : string -> string -> int option -> unit
    3.20 +end;
    3.21 +
    3.22 +structure Async_Manager : ASYNC_MANAGER =
    3.23 +struct
    3.24 +
    3.25 +(** preferences **)
    3.26 +
    3.27 +val message_store_limit = 20;
    3.28 +val message_display_limit = 5;
    3.29 +
    3.30 +
    3.31 +(** thread management **)
    3.32 +
    3.33 +(* data structures over threads *)
    3.34 +
    3.35 +structure Thread_Heap = Heap
    3.36 +(
    3.37 +  type elem = Time.time * Thread.thread;
    3.38 +  fun ord ((a, _), (b, _)) = Time.compare (a, b);
    3.39 +);
    3.40 +
    3.41 +fun lookup_thread xs = AList.lookup Thread.equal xs;
    3.42 +fun delete_thread xs = AList.delete Thread.equal xs;
    3.43 +fun update_thread xs = AList.update Thread.equal xs;
    3.44 +
    3.45 +
    3.46 +(* state of thread manager *)
    3.47 +
    3.48 +type state =
    3.49 +  {manager: Thread.thread option,
    3.50 +   timeout_heap: Thread_Heap.T,
    3.51 +   active: (Thread.thread * (string * Time.time * Time.time * string)) list,
    3.52 +   canceling: (Thread.thread * (string * Time.time * string)) list,
    3.53 +   messages: (string * string) list,
    3.54 +   store: (string * string) list}
    3.55 +
    3.56 +fun make_state manager timeout_heap active canceling messages store : state =
    3.57 +  {manager = manager, timeout_heap = timeout_heap, active = active,
    3.58 +   canceling = canceling, messages = messages, store = store}
    3.59 +
    3.60 +val global_state = Synchronized.var "async_manager"
    3.61 +  (make_state NONE Thread_Heap.empty [] [] [] []);
    3.62 +
    3.63 +
    3.64 +(* unregister thread *)
    3.65 +
    3.66 +fun unregister verbose message thread =
    3.67 +  Synchronized.change global_state
    3.68 +  (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
    3.69 +    (case lookup_thread active thread of
    3.70 +      SOME (tool, birth_time, _, desc) =>
    3.71 +        let
    3.72 +          val active' = delete_thread thread active;
    3.73 +          val now = Time.now ()
    3.74 +          val canceling' = (thread, (tool, now, desc)) :: canceling
    3.75 +          val message' =
    3.76 +            desc ^ "\n" ^ message ^
    3.77 +            (if verbose then
    3.78 +               "\nTotal time: " ^ Int.toString (Time.toMilliseconds
    3.79 +                                            (Time.- (now, birth_time))) ^ " ms."
    3.80 +             else
    3.81 +               "")
    3.82 +          val messages' = (tool, message') :: messages;
    3.83 +          val store' = (tool, message') ::
    3.84 +            (if length store <= message_store_limit then store
    3.85 +             else #1 (chop message_store_limit store));
    3.86 +        in make_state manager timeout_heap active' canceling' messages' store' end
    3.87 +    | NONE => state));
    3.88 +
    3.89 +
    3.90 +(* main manager thread -- only one may exist *)
    3.91 +
    3.92 +val min_wait_time = Time.fromMilliseconds 300;
    3.93 +val max_wait_time = Time.fromSeconds 10;
    3.94 +
    3.95 +fun replace_all bef aft =
    3.96 +  let
    3.97 +    fun aux seen "" = String.implode (rev seen)
    3.98 +      | aux seen s =
    3.99 +        if String.isPrefix bef s then
   3.100 +          aux seen "" ^ aft ^ aux [] (unprefix bef s)
   3.101 +        else
   3.102 +          aux (String.sub (s, 0) :: seen) (String.extract (s, 1, NONE))
   3.103 +  in aux [] end
   3.104 +
   3.105 +(* This is a workaround for Proof General's off-by-a-few sendback display bug,
   3.106 +   whereby "pr" in "proof" is not highlighted. *)
   3.107 +fun break_into_chunks xs =
   3.108 +  maps (space_explode "\000" o replace_all "\n\n" "\000" o snd) xs
   3.109 +
   3.110 +fun print_new_messages () =
   3.111 +  case Synchronized.change_result global_state
   3.112 +         (fn {manager, timeout_heap, active, canceling, messages, store} =>
   3.113 +             (messages, make_state manager timeout_heap active canceling []
   3.114 +                                   store)) of
   3.115 +    [] => ()
   3.116 +  | msgs as (tool, _) :: _ =>
   3.117 +    let val ss = break_into_chunks msgs in
   3.118 +      List.app priority (tool ^ ": " ^ hd ss :: tl ss)
   3.119 +    end
   3.120 +
   3.121 +fun check_thread_manager verbose = Synchronized.change global_state
   3.122 +  (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
   3.123 +    if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state
   3.124 +    else let val manager = SOME (Toplevel.thread false (fn () =>
   3.125 +      let
   3.126 +        fun time_limit timeout_heap =
   3.127 +          (case try Thread_Heap.min timeout_heap of
   3.128 +            NONE => Time.+ (Time.now (), max_wait_time)
   3.129 +          | SOME (time, _) => time);
   3.130 +
   3.131 +        (*action: find threads whose timeout is reached, and interrupt canceling threads*)
   3.132 +        fun action {manager, timeout_heap, active, canceling, messages, store} =
   3.133 +          let val (timeout_threads, timeout_heap') =
   3.134 +            Thread_Heap.upto (Time.now (), Thread.self ()) timeout_heap;
   3.135 +          in
   3.136 +            if null timeout_threads andalso null canceling then
   3.137 +              NONE
   3.138 +            else
   3.139 +              let
   3.140 +                val _ = List.app (Simple_Thread.interrupt o #1) canceling
   3.141 +                val canceling' = filter (Thread.isActive o #1) canceling
   3.142 +                val state' = make_state manager timeout_heap' active canceling' messages store;
   3.143 +              in SOME (map #2 timeout_threads, state') end
   3.144 +          end;
   3.145 +      in
   3.146 +        while Synchronized.change_result global_state
   3.147 +          (fn state as {timeout_heap, active, canceling, messages, store, ...} =>
   3.148 +            if null active andalso null canceling andalso null messages
   3.149 +            then (false, make_state NONE timeout_heap active canceling messages store)
   3.150 +            else (true, state))
   3.151 +        do
   3.152 +          (Synchronized.timed_access global_state (SOME o time_limit o #timeout_heap) action
   3.153 +            |> these
   3.154 +            |> List.app (unregister verbose "Timed out.\n");
   3.155 +            print_new_messages ();
   3.156 +            (*give threads some time to respond to interrupt*)
   3.157 +            OS.Process.sleep min_wait_time)
   3.158 +      end))
   3.159 +    in make_state manager timeout_heap active canceling messages store end)
   3.160 +
   3.161 +
   3.162 +(* register thread *)
   3.163 +
   3.164 +fun register tool verbose birth_time death_time desc thread =
   3.165 + (Synchronized.change global_state
   3.166 +    (fn {manager, timeout_heap, active, canceling, messages, store} =>
   3.167 +      let
   3.168 +        val timeout_heap' = Thread_Heap.insert (death_time, thread) timeout_heap;
   3.169 +        val active' = update_thread (thread, (tool, birth_time, death_time, desc)) active;
   3.170 +        val state' = make_state manager timeout_heap' active' canceling messages store;
   3.171 +      in state' end);
   3.172 +  check_thread_manager verbose);
   3.173 +
   3.174 +
   3.175 +fun launch tool verbose birth_time death_time desc f =
   3.176 +  (Toplevel.thread true
   3.177 +       (fn () =>
   3.178 +           let
   3.179 +             val self = Thread.self ()
   3.180 +             val _ = register tool verbose birth_time death_time desc self
   3.181 +             val message = f ()
   3.182 +           in unregister verbose message self end);
   3.183 +   ())
   3.184 +
   3.185 +
   3.186 +(** user commands **)
   3.187 +
   3.188 +(* kill threads *)
   3.189 +
   3.190 +fun kill_threads tool workers = Synchronized.change global_state
   3.191 +  (fn {manager, timeout_heap, active, canceling, messages, store} =>
   3.192 +    let
   3.193 +      val killing =
   3.194 +        map_filter (fn (th, (tool', _, _, desc)) =>
   3.195 +                       if tool' = tool then SOME (th, (tool', Time.now (), desc))
   3.196 +                       else NONE) active
   3.197 +      val state' = make_state manager timeout_heap [] (killing @ canceling) messages store;
   3.198 +      val _ = if null killing then () else priority ("Killed active " ^ workers ^ ".")
   3.199 +    in state' end);
   3.200 +
   3.201 +
   3.202 +(* running threads *)
   3.203 +
   3.204 +fun seconds time = string_of_int (Time.toSeconds time) ^ " s"
   3.205 +
   3.206 +fun running_threads tool workers =
   3.207 +  let
   3.208 +    val {active, canceling, ...} = Synchronized.value global_state;
   3.209 +
   3.210 +    val now = Time.now ();
   3.211 +    fun running_info (_, (tool', birth_time, death_time, desc)) =
   3.212 +      if tool' = tool then
   3.213 +        SOME ("Running: " ^ seconds (Time.- (now, birth_time)) ^ " -- " ^
   3.214 +              seconds (Time.- (death_time, now)) ^ " to live:\n" ^ desc)
   3.215 +      else
   3.216 +        NONE
   3.217 +    fun canceling_info (_, (tool', death_time, desc)) =
   3.218 +      if tool' = tool then
   3.219 +        SOME ("Trying to interrupt thread since " ^
   3.220 +              seconds (Time.- (now, death_time)) ^ ":\n" ^ desc)
   3.221 +      else
   3.222 +        NONE
   3.223 +    val running =
   3.224 +      case map_filter running_info active of
   3.225 +        [] => ["No " ^ workers ^ " running."]
   3.226 +      | ss => "Running " ^ workers ^ ":" :: ss
   3.227 +    val interrupting =
   3.228 +      case map_filter canceling_info canceling of
   3.229 +        [] => []
   3.230 +      | ss => "Trying to interrupt the following " ^ workers ^ ":" :: ss
   3.231 +  in priority (space_implode "\n\n" (running @ interrupting)) end
   3.232 +
   3.233 +fun thread_messages tool worker opt_limit =
   3.234 +  let
   3.235 +    val limit = the_default message_display_limit opt_limit;
   3.236 +    val tool_store = Synchronized.value global_state
   3.237 +                     |> #store |> filter (curry (op =) tool o fst)
   3.238 +    val header =
   3.239 +      "Recent " ^ worker ^ " messages" ^
   3.240 +        (if length tool_store <= limit then ":"
   3.241 +         else " (" ^ string_of_int limit ^ " displayed):");
   3.242 +  in List.app priority (header :: break_into_chunks (#1 (chop limit tool_store))) end
   3.243 +
   3.244 +end;