Scheduler ->
  sig
    val register_observer : (int -> int -> int -> unit) -> unit
    val interrupt : Controller_itp.controller -> unit
    val interrupt_proof_attempts_for_goal :
      Controller_itp.controller -> Session_itp.proofNodeID -> unit
    val schedule_proof_attempt :
      ?proof_script_filename:string ->
      Controller_itp.controller ->
      Session_itp.proofNodeID ->
      Whyconf.prover ->
      limit:Call_provers.resource_limit ->
      callback:(Session_itp.proofAttemptID ->
                Controller_itp.proof_attempt_status -> unit) ->
      notification:Session_itp.notifier -> unit
    val schedule_edition :
      Controller_itp.controller ->
      Session_itp.proofNodeID ->
      Whyconf.prover ->
      callback:(Session_itp.proofAttemptID ->
                Controller_itp.proof_attempt_status -> unit) ->
      notification:Session_itp.notifier -> unit
    val prepare_edition :
      Controller_itp.controller ->
      ?file:Sysutil.file_path ->
      Session_itp.proofNodeID ->
      Whyconf.prover ->
      notification:Session_itp.notifier ->
      Session_itp.proofAttemptID * string * Call_provers.prover_result option
    exception GoalNodeDetached of Session_itp.proofNodeID
    val schedule_transformation :
      Controller_itp.controller ->
      Session_itp.proofNodeID ->
      string ->
      string list ->
      callback:(Controller_itp.transformation_status -> unit) ->
      notification:Session_itp.notifier -> unit
    val run_strategy_on_goal :
      Controller_itp.controller ->
      Session_itp.proofNodeID ->
      Strategy.t ->
      callback_pa:(Session_itp.proofAttemptID ->
                   Controller_itp.proof_attempt_status -> unit) ->
      callback_tr:(string ->
                   string list ->
                   Controller_itp.transformation_status -> unit) ->
      callback:(Controller_itp.strategy_status -> unit) ->
      notification:Session_itp.notifier ->
      removed:Session_itp.notifier -> unit
    val run_strat_on_goal :
      Controller_itp.controller ->
      Session_itp.proofNodeID ->
      (Env.env -> Task.task -> Strategy.strat) ->
      callback_pa:(Session_itp.proofAttemptID ->
                   Controller_itp.proof_attempt_status -> unit) ->
      callback_tr:(string ->
                   string list ->
                   Controller_itp.transformation_status -> unit) ->
      callback:(Controller_itp.strategy_status -> unit) ->
      notification:Session_itp.notifier -> unit
    val clean :
      Controller_itp.controller ->
      removed:Session_itp.notifier -> Session_itp.any option -> unit
    val reset_proofs :
      Controller_itp.controller ->
      removed:Session_itp.notifier ->
      notification:Session_itp.notifier -> Session_itp.any option -> unit
    val mark_as_obsolete :
      notification:Session_itp.notifier ->
      Controller_itp.controller -> Session_itp.any option -> unit
    exception BadCopyPaste
    val copy_paste :
      notification:Session_itp.notifier ->
      callback_pa:(Session_itp.proofAttemptID ->
                   Controller_itp.proof_attempt_status -> unit) ->
      callback_tr:(string ->
                   string list ->
                   Controller_itp.transformation_status -> unit) ->
      Controller_itp.controller -> Session_itp.any -> Session_itp.any -> unit
    type report =
        Result of Call_provers.prover_result * Call_provers.prover_result
      | CallFailed of exn
      | Replay_interrupted
      | Prover_not_installed
      | Edited_file_absent of string
      | No_former_result of Call_provers.prover_result
    val replay_print :
      Stdlib.Format.formatter ->
      (Session_itp.proofNodeID * Whyconf.prover *
       Call_provers.resource_limit * Controller_itp.Make.report)
      list -> unit
    val replay :
      valid_only:bool ->
      obsolete_only:bool ->
      ?use_steps:bool ->
      ?filter:(Session_itp.proof_attempt_node -> bool) ->
      Controller_itp.controller ->
      callback:(Session_itp.proofAttemptID ->
                Controller_itp.proof_attempt_status -> unit) ->
      notification:Session_itp.notifier ->
      final_callback:(bool ->
                      (Session_itp.proofNodeID * Whyconf.prover *
                       Call_provers.resource_limit *
                       Controller_itp.Make.report)
                      list -> unit) ->
      any:Session_itp.any option -> unit
    exception CannotRunBisectionOn of Session_itp.proofAttemptID
    val bisect_proof_attempt :
      callback_tr:(string ->
                   string list ->
                   Controller_itp.transformation_status -> unit) ->
      callback_pa:(Session_itp.proofAttemptID ->
                   Controller_itp.proof_attempt_status -> unit) ->
      notification:Session_itp.notifier ->
      removed:Session_itp.notifier ->
      Controller_itp.controller -> Session_itp.proofAttemptID -> unit
  end