vscoq-language-server 2.2.1 (latest)

The event manager is in charge of the actual event of tasks (as defined by the scheduler), caching event states and invalidating them. It can delegate to worker processes via DelegationManager

type delegation_mode =

| CheckProofsInMaster
| SkipProofs
| DelegateProofsToWorkers of {
1. number_of_workers : int;
}

type options = {

delegation_mode : delegation_mode;
completion_options : Protocol.Settings.Completion.t;
enableDiagnostics : bool;

}

val is_diagnostics_enabled : unit -> bool

type state

Execution state, includes the cache

type event

type events = event Sel.Event.t list

type errored_sentence = Types.sentence_id option

type feedback_message =
  Feedback.level * Loc.t option * Types.Quickfix.t list * Pp.t

val pr_event : event -> Pp.t

val init : Vernacstate.t -> state * event Sel.Event.t

val destroy : state -> unit

val get_options : unit -> options

val set_options : options -> unit

val set_default_options : unit -> unit

val invalidate : 
  Document.document ->
  Scheduler.schedule ->
  Types.sentence_id ->
  state ->
  state

val error : state -> Types.sentence_id -> (Loc.t option * Pp.t) option

val feedback : state -> Types.sentence_id -> feedback_message list

val all_errors : 
  state ->
  (Types.sentence_id * (Loc.t option * Pp.t * Types.Quickfix.t list option))
    list

val all_feedback : state -> (Types.sentence_id * feedback_message) list

val shift_overview : 
  state ->
  before:RawDocument.t ->
  after:RawDocument.t ->
  start:int ->
  offset:int ->
  state

val shift_diagnostics_locs : state -> start:int -> offset:int -> state

val executed_ids : state -> Types.sentence_id list

val is_executed : state -> Types.sentence_id -> bool

val is_remotely_executed : state -> Types.sentence_id -> bool

val get_context : 
  state ->
  Types.sentence_id ->
  (Evd.evar_map * Environ.env) option

val get_initial_context : state -> Evd.evar_map * Environ.env

val get_vernac_state : state -> Types.sentence_id -> Vernacstate.t option

Returns the vernac state after the sentence

val handle_event : 
  event ->
  state ->
  Types.sentence_id option * state option * events

Events for the main loop

type prepared_task

Execution happens in two steps. In particular the event one takes only one task at a time to ease checking for interruption

val build_tasks_for : 
  Document.document ->
  Scheduler.schedule ->
  state ->
  Types.sentence_id ->
  bool ->
  Vernacstate.t * prepared_task list * state * Types.sentence_id option

val execute : 
  state ->
  (Vernacstate.t * events * bool) ->
  prepared_task ->
  state * Vernacstate.t * events * bool * errored_sentence

val update_overview : 
  prepared_task ->
  prepared_task list ->
  state ->
  Document.document ->
  state

val cut_overview : prepared_task -> state -> Document.document -> state

val update_processed : Types.sentence_id -> state -> Document.document -> state

val prepare_overview : state -> Protocol.LspWrapper.Range.t list -> state

val overview : state -> Types.exec_overview

val overview_until_range : 
  state ->
  Protocol.LspWrapper.Range.t ->
  Types.exec_overview

val print_exec_overview_of_state : state -> unit

module ProofWorkerProcess : sig ... end

Coq toplevels for delegation without fork

package vscoq-language-server