deferred class JOB

Features exported to LOOP_ITEM

The job life will looks like : 

  do
     prepare
     if is_ready then
        continue
  repeat while not done
If the same job as to live again, restart is called.

Note: never change priority after job inserted in loop_item. 

      Priority should only be set at creation time.

Direct parents

non-conformant parents

ANY, PLATFORM

Known children

conformant children

BACKGROUND_JOB, CONNECTION, EVENT_CATCHER, PERIODIC_JOB, SOCKET_SERVER_JOB

Summary

exported features

Details

priority: INTEGER

Never change priority after job inserted in loop_item. Priority should only be set at creation time.

deferred prepare (ready: READY_DESCRIPTION)

use ready to descibe condition that make this job ready to continue.

require

  • ready /= Void
  • not ready.queryable

deferred is_ready (ready: READY_DESCRIPTION): BOOLEAN

check if this job is ready to continue his work

require

  • ready /= Void
  • ready.queryable

deferred continue

Continue to do the job The work to do has to be small work and non blocking, it will continue on next call

deferred done: BOOLEAN

done returns True when the job is finished. Then the job may be restart(ed) if it need to run again.

deferred restart

Configure the job like the initial state. Example: when some window dialog appears second time, all jobs from this window are restarted.

require

  • done

ensure

  • not done

< (other: JOB): BOOLEAN

Class invariant