package vscoq-language-server

  1. Overview
  2. Docs
VSCoq language server

Install 

dune-project
 Dependency

github.com Readme Edit opam file Versions (14)

Authors

  1. E
    Enrico Tassi
  2. M
    Maxime Dénès
  3. R
    Romain Tetley

Maintainers

  1. E
    Enrico Tassi <enrico.tassi@inria.fr>

Sources

vscoq-language-server-2.0.2-coq8.18.tar.gz
md5=8a4ff41372c157688170f0174e58d646
sha512=852f4e8cc7e687805e0707368a5625ef3c226d1373f677a731d32a04f8d0cb2f5d64ffdf350b0a5e446ff5075982dc36f2bc9d533d3862009f73fc22fd04fcc0

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

Module Dm.DocumentManagerSource

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 state
Sourcetype event
Sourceval pp_event : Format.formatter -> event -> unit
Sourcetype events = event Sel.Event.t list

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

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.

Sourceval interpret_to_position : stateful:bool -> state -> Protocol.LspWrapper.Position.t -> state * events

interpret_to_position stateful doc pos navigates to the last sentence ending before or at pos and returns the resulting state. The stateful flag determines if we record the resulting position in the state.

Sourceval interpret_to_previous : state -> state * events

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

Sourceval interpret_to_next : state -> state * events

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

Sourceval interpret_to_end : state -> state * events

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

Sourceval interpret_in_background : state -> 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

Sourcetype exec_overview = {
  1. parsed : Protocol.LspWrapper.Range.t list;
  2. checked : Protocol.LspWrapper.Range.t list;
  3. checked_by_delegate : Protocol.LspWrapper.Range.t list;
  4. legacy_highlight : Protocol.LspWrapper.Range.t list;
}
Sourceval executed_ranges : state -> exec_overview

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

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

returns the range of the sentence referenced by observe_id *

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.

Sourceval handle_event : event -> state -> state option * events

handles events and returns a new state if it was updated

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

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

Sourceval check : state -> Protocol.LspWrapper.Position.t -> pattern:string -> (Protocol.Printing.pp, string) Result.t
Sourceval locate : state -> Protocol.LspWrapper.Position.t -> pattern:string -> (Protocol.Printing.pp, string) Result.t
Sourceval print : state -> Protocol.LspWrapper.Position.t -> pattern:string -> (Protocol.Printing.pp, string) Result.t
Sourcemodule Internal : sig ... end