vscoq-language-server 2.2.1 (latest)

The document manager holds the view that Coq has of the currently open states. It makes it easy for IDEs to handle text edits, navigate and get feedback. Note that it does not require IDEs to parse vernacular sentences.

type observe_id =

| Id of Types.sentence_id
| Top

type blocking_error = {

last_range : Protocol.LspWrapper.Range.t;
error_range : Protocol.LspWrapper.Range.t;

}

type state

type event

val pp_event : Stdlib.Format.formatter -> event -> unit

type events = event Sel.Event.t list

val init : 
  Vernacstate.t ->
  opts:Coqargs.injection_command list ->
  Lsp.Types.DocumentUri.t ->
  text:string ->
  observe_id option ->
  state * events

init st opts uri text initializes the document manager with initial vernac state st on which command line opts will be set.

val apply_text_edits : state -> Types.text_edit list -> state

apply_text_edits doc edits updates the text of doc with edits. The new document is parsed, outdated executions states are invalidated, and the observe id is updated.

val clear_observe_id : state -> state

clear_observe_id state updates the state to make the observe_id None

val reset_to_top : state -> state

reset_to_top state updates the state to make the observe_id Top

val get_next_range : 
  state ->
  Protocol.LspWrapper.Position.t ->
  Protocol.LspWrapper.Range.t option

get_next_range st pos get the range of the next sentence relative to pos

val get_previous_range : 
  state ->
  Protocol.LspWrapper.Position.t ->
  Protocol.LspWrapper.Range.t option

get_previous_pos st pos get the range of the previous sentence relative to pos

val interpret_to_position : 
  state ->
  Protocol.LspWrapper.Position.t ->
  should_block_on_error:bool ->
  state * events * blocking_error option

interpret_to_position state pos should_block navigates to the last sentence ending before or at pos and returns the resulting state, events that need to take place, and a possible blocking error.

val interpret_to_next_position : 
  state ->
  Protocol.LspWrapper.Position.t ->
  should_block_on_error:bool ->
  state * events * blocking_error option * Protocol.LspWrapper.Position.t

interpret_to_next_position state pos should_block navigates to the first sentence after or at pos (excluding whitespace) and returns the resulting state, events that need to take place, a possible blocking error, and the position of the sentence that was interpreted until.

val interpret_to_previous : state -> state * events * blocking_error option

interpret_to_previous doc navigates to the previous sentence in doc and returns the resulting state.

val interpret_to_next : 
  state ->
  should_block_on_error:bool ->
  state * events * blocking_error option

interpret_to_next doc navigates to the next sentence in doc and returns the resulting state.

val interpret_to_end : 
  state ->
  should_block_on_error:bool ->
  state * events * blocking_error option

interpret_to_end doc navigates to the last sentence in doc and returns the resulting state.

val interpret_in_background : 
  state ->
  should_block_on_error:bool ->
  state * events * blocking_error option

interpret_in_background doc same as interpret_to_end but computation is done in background (with lower priority)

val reset : state -> state * events

resets Coq

val executed_ranges : state -> Types.exec_overview

returns the ranges corresponding to the sentences that have been executed and remotely executes

val observe_id_range : state -> Protocol.LspWrapper.Range.t option

returns the range of the sentence referenced by observe_id *

val get_messages : 
  state ->
  Protocol.LspWrapper.Position.t option ->
  (Protocol.LspWrapper.DiagnosticSeverity.t * Protocol.Printing.pp) list

returns the messages associated to a given position

val get_info_messages : 
  state ->
  Protocol.LspWrapper.Position.t option ->
  (Protocol.LspWrapper.DiagnosticSeverity.t * Protocol.Printing.pp) list

returns the Feedback.Info level messages associated to a given position

val get_document_symbols : state -> Lsp.Types.DocumentSymbol.t list

val all_diagnostics : state -> Lsp.Types.Diagnostic.t list

all_diagnostics doc returns the diagnostics corresponding to the sentences that have been executed in doc.

val get_proof : 
  state ->
  Protocol.Settings.Goals.Diff.Mode.t ->
  Protocol.LspWrapper.Position.t option ->
  Protocol.ProofState.t option

val get_completions : 
  state ->
  Protocol.LspWrapper.Position.t ->
  (CompletionItems.completion_item list, string) Stdlib.Result.t

val handle_event : 
  event ->
  state ->
  bool ->
  state option * events * blocking_error option

handles events and returns a new state if it was updated

val search : 
  state ->
  id:string ->
  Protocol.LspWrapper.Position.t ->
  string ->
  Protocol.LspWrapper.notification Sel.Event.t list

val about : 
  state ->
  Protocol.LspWrapper.Position.t ->
  pattern:string ->
  (Protocol.Printing.pp, string) Stdlib.Result.t

val hover : 
  state ->
  Protocol.LspWrapper.Position.t ->
  Lsp.Types.MarkupContent.t option

Returns an optional Result: if None, the position did not have a word, if Some, an Ok/Error result is returned.

val check : 
  state ->
  Protocol.LspWrapper.Position.t ->
  pattern:string ->
  (Protocol.Printing.pp, string) Stdlib.Result.t

val locate : 
  state ->
  Protocol.LspWrapper.Position.t ->
  pattern:string ->
  (Protocol.Printing.pp, string) Stdlib.Result.t

val print : 
  state ->
  Protocol.LspWrapper.Position.t ->
  pattern:string ->
  (Protocol.Printing.pp, string) Stdlib.Result.t

module Internal : sig ... end

package vscoq-language-server