package vscoq-language-server

  1. Overview
  2. Docs

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 =
  1. | CheckProofsInMaster
  2. | SkipProofs
  3. | DelegateProofsToWorkers of {
    1. number_of_workers : int;
    }
type options = {
  1. delegation_mode : delegation_mode;
  2. completion_options : Protocol.Settings.Completion.t;
  3. 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 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

OCaml

Innovation. Community. Security.