From: Richard W.M. Jones Date: Mon, 20 Jan 2020 12:20:04 +0000 (+0000) Subject: jobs: Remove unnecessary 'a retire and 'a to_string types. X-Git-Url: http://git.annexia.org/?a=commitdiff_plain;h=614e2b7de8284ed70c004f5f2847d868c8e40e3b;p=goals.git jobs: Remove unnecessary 'a retire and 'a to_string types. --- diff --git a/src/jobs.ml b/src/jobs.ml index 2e8735e..249ab6a 100644 --- a/src/jobs.ml +++ b/src/jobs.ml @@ -21,10 +21,6 @@ open Utils type 'a next = Job of 'a * (unit -> unit) | Complete | Not_ready -type 'a retire = 'a -> unit - -type 'a to_string = 'a -> string - let run next_job retire_job string_of_job = (* Number of running threads <= Cmdline.nr_jobs. *) let running = ref 0 in diff --git a/src/jobs.mli b/src/jobs.mli index 8aedbba..a5b79bb 100644 --- a/src/jobs.mli +++ b/src/jobs.mli @@ -21,14 +21,12 @@ type 'a next = Job of 'a * (unit -> unit) | Complete | Not_ready -type 'a retire = 'a -> unit +val run : (unit -> 'a next) -> ('a -> unit) -> ('a -> string) -> unit +(** [run next_job retire_job to_string] runs jobs in parallel. -type 'a to_string = 'a -> string - -val run : (unit -> 'a next) -> 'a retire -> 'a to_string -> unit -(** [run next_job retire_job] runs jobs in parallel. [next_job] - is called to pick the next available job. [retire_job] is - called when a job finishes successfully. + [next_job] is called to pick the next available job. + [retire_job] is called when a job finishes successfully. + [to_string] is called if we need to print the job name. If [next_job] returns [Job f] then that function is started (usually in a thread if -j N > 1).