X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;f=src%2Fjobs.mli;h=9be4186cbcbf523a2cf601610540ffd4a893eb8f;hb=4f3f374e059fd46d40f3058c4e65e63aa4ac56cb;hp=8aedbba9c6baef4346e3a91b0c1c1e3d8df977d9;hpb=a70987f316ab4b948bf941ddea8fb6ccef09da4f;p=goals.git diff --git a/src/jobs.mli b/src/jobs.mli index 8aedbba..9be4186 100644 --- a/src/jobs.mli +++ b/src/jobs.mli @@ -21,20 +21,22 @@ type 'a next = Job of 'a * (unit -> unit) | Complete | Not_ready -type 'a retire = 'a -> unit +val run : (unit -> 'a next) -> ('a -> unit) -> ('a -> unit) -> + ('a -> string) -> unit +(** [run next_job retire_job fail_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. + [fail_job] is called when a job fails (only in keep-going + -k mode). All jobs that depend on this one must be marked + failed by the caller. + [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). If [next_job] returns [Complete] then [run] waits until - all parallel jobs are then returns. + all parallel jobs are finished then returns. If [next_job] returns [Not_ready] then [next_job] will be called again after a little while. @@ -42,4 +44,5 @@ val run : (unit -> 'a next) -> 'a retire -> 'a to_string -> unit If any job throws an exception then the exception will be reraised by [run], usually causing goals to exit with an error. The exception is delayed until all currently running jobs - finish, but no new jobs will be started during this time. *) + finish. In normal mode no new jobs will be started during + this time. In keep-going -k mode new jobs may be started. *)