Module `Dm.DocumentManager`Source

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.

Sourcetype observe_id =

| Id of Types.sentence_id
| Top

Sourcetype blocking_error = {

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

}

Sourcetype state

Sourcetype event

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

Sourcetype events = event Sel.Event.t list

Sourcetype handled_event = {

state : state option;
events : events;
update_view : bool;
notification : Protocol.ExtProtocol.Notification.Server.t option;

}

Sourceval is_parsing : state -> bool

Source

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

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

Sourceval apply_text_edits : state -> Types.text_edit list -> state * events

apply_text_edits doc edits updates the text of doc with edits. A ParseEvent is triggered, once processed: the new document is parsed, outdated executions states are invalidated, and the observe id is updated.

Sourceval reset_to_top : state -> state

reset_to_top state updates the state to make the observe_id Top

Source

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

Source

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

Source

val interpret_to_position : 
  state ->
  Protocol.LspWrapper.Position.t ->
  Protocol.Settings.Mode.t ->
  point_interp_mode:Protocol.Settings.PointInterpretationMode.t ->
  state * events

interpret_to_position state pos check_mode point_interp_mode 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.

Source

val interpret_to_next_position : 
  state ->
  Protocol.LspWrapper.Position.t ->
  Protocol.Settings.Mode.t ->
  state * events

interpret_to_next_position state pos check_mode 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.

Sourceval interpret_to_previous : state -> Protocol.Settings.Mode.t -> state * events

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

Sourceval interpret_to_next : state -> Protocol.Settings.Mode.t -> state * events

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

Sourceval interpret_to_end : state -> Protocol.Settings.Mode.t -> state * events

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

Source

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

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

Sourceval reset : state -> state * events

resets Coq

Sourceval executed_ranges : state -> Protocol.Settings.Mode.t -> Types.exec_overview

executes_ranges doc mode returns the ranges corresponding to the sentences that have been executed. mode allows to send a "cut" range that only goes until the observe_id in the case of manual mode

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

returns the range of the sentence referenced by observe_id *

Source

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

returns the messages associated to a given position

Source

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

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

Sourceval get_document_proofs : state -> Protocol.ProofState.proof_block list

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

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

Source

val get_proof : 
  state ->
  Protocol.Settings.Goals.Diff.Mode.t ->
  Types.sentence_id option ->
  Protocol.ProofState.t option

Source

val get_completions : 
  state ->
  Protocol.LspWrapper.Position.t ->
  CompletionItems.completion_item list

Source

val handle_event : 
  event ->
  state ->
  block:bool ->
  Protocol.Settings.Mode.t ->
  Protocol.Settings.Goals.Diff.Mode.t ->
  handled_event

handles events and returns a new state if it was updated. On top of the next events, it also returns info on whether execution has halted due to an error and returns a boolean flag stating whether the view should be updated

Source

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

Source

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

Source

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.

Source

val jump_to_definition : 
  state ->
  Protocol.LspWrapper.Position.t ->
  (Protocol.LspWrapper.Range.t * string) option

Source

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

Source

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

Source

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

Sourcemodule Internal : sig ... end

Install

Dune Dependency

Authors

Maintainers

Sources

doc/vscoq-language-server.dm/Dm/DocumentManager/index.html

Module `Dm.DocumentManager`Source

package vscoq-language-server

Install

Dune Dependency

Authors

Maintainers

Sources

doc/vscoq-language-server.dm/Dm/DocumentManager/index.html

Module Dm.DocumentManagerSource

Module `Dm.DocumentManager`Source