Module VernacControl

type 'state control_entry

Partially interpreted control flags.

type 'state control_entries = 'state control_entry list
val from_syntax : Vernacexpr.control_flag list -> unit control_entries

Translate from syntax and add default timeout.

type ('st0, 'st) with_local_state = {
with_local_state : a. 'st0 -> (unit -> 'a) -> 'st * 'a;
}

with_local_state state0 f should run f with state0 installed, capture the state produced by running f and revert the global state afterwards.

val trivial_state : (unit, unit) with_local_state
val under_control : loc:Loc.t option -> with_local_state:('state0, 'state) with_local_state -> 'state0 control_entries -> noop:'b -> (unit -> 'b) -> 'state control_entries * 'b

under_control ~loc ~with_local_state control ~noop f runs f () in the context given by the control.

If the control cause execution to end with no more work to be done and no error (eg Fail when f raised an exception) then noop is returned.

val after_last_phase : loc:Loc.t option -> _ control_entries -> bool

Print any final messages (eg from Time) and raise final exceptions (eg from Fail when the command did not fail). The returned boolean tells if we should be noop (Fail where the command failed or Succeed where it succeeded).

exception CmdTimeout

Exposed so that waterproof can change the error message.