Module `Dm.CheckingManager`Source

Sourcetype settings = {

}

Sourceval set_options : settings -> unit

Sourcetype event

Sourceval pp_event : Format.formatter -> event -> unit

Sourcetype state

Sourceval init : feedback_pipe:Types.feedback_pipe -> Vernacstate.t -> state

val reset : 
  state ->
  Vernacstate.t ->
  feedback_pipe:Types.feedback_pipe ->
  state

Sourceval reset_to_top : state -> state

reset_to_top state updates the state to make the observe_id Top

Sourceval get_observe_id : state -> Types.sentence_id option

val reset_overview : 
  state ->
  Document.document ->
  Types.sentence_id option ->
  state

Sourceval overview : state -> Types.exec_overview

val shift_overview : 
  state ->
  before:Document.document ->
  after:Document.document ->
  start:int ->
  offset:int ->
  state

Sourceval executed_ranges : Document.document -> state -> Types.exec_overview

Sourceval observe_id_range : Document.document -> state -> Lsp.Types.Range.t option

Sourceval interpret_to_end : unit -> event Sel.Event.t list

Sourceval interpret_to_next : unit -> event Sel.Event.t list

Sourceval interpret_to_previous : unit -> event Sel.Event.t list

Sourceval interpret_to_position : Lsp.Types.Position.t -> event Sel.Event.t list

val interpret_in_background : 
  Document.document ->
  state ->
  state * event Sel.Event.t list

Sourceval invalidate : state -> Types.sentence_id -> state

val validate_document : 
  Document.document ->
  state ->
  state * event Sel.Event.t list

val vernac_state_of_sentence : 
  Document.document ->
  Types.sentence_id ->
  Vernacstate.t option

val get_proof : 
  Document.document ->
  state ->
  Types.sentence_id option ->
  Protocol.ProofState.t option

val get_messages : 
  Document.document ->
  Types.sentence_id ->
  (Lsp.Types.DiagnosticSeverity.t * Protocol.Printing.pp) list

val handle_event : 
  uri:Lsp.Uri.t ->
  Document.document ->
  state ->
  event ->
  Types.document_updates * (state, event) Types.handled_event

Sourcemodule Internal : sig ... end

Install