package vscoq-language-server

  1. Overview
  2. Docs
VSCoq language server

Install 

dune-project
 Dependency

github.com Readme Edit opam file Versions (15)

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.1.0-coq8.19.tar.gz
md5=7bdc4ae44d8d6ab21d586e20835a1b79
sha512=7ab8ddae303a9b9ec2d62338edbf4176ca1146ed29e34eb02cf41fc91bf21d507c6e571ba30b73e45869d25a750d7915e79b915d962629cb9aed1598e0b68795

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

Module Dm.DocumentSource

This file defines operations on the content of a document (text, parsing of sentences, scheduling).

Sourcetype document

The document gathers the text, which is partially validated (parsed into sentences

Sourceval raw_document : document -> RawDocument.t
Sourceval create_document : Vernacstate.Synterp.t -> string -> document

create_document init_synterp_state text creates a fresh document with content defined by text under init_synterp_state.

Sourceval validate_document : document -> Types.sentence_id option * Types.sentence_id_set * document

validate_document doc parses the document without forcing any execution and returns the id of the bottommost sentence of the prefix which has not changed since the previous validation, as well as the set of invalidated sentences

Sourcetype parsed_ast = {
  1. ast : Synterp.vernac_control_entry;
  2. classification : Vernacextend.vernac_classification;
  3. tokens : Tok.t list;
}
Sourcetype parsing_error = {
  1. start : int;
  2. stop : int;
  3. msg : string Loc.located;
}
Sourceval parse_errors : document -> parsing_error list

parse_errors doc returns the list of sentences which failed to parse (see validate_document) together with their error message

Sourceval apply_text_edits : document -> Types.text_edit list -> document

apply_text_edits doc edits updates the text of doc with edits. The new text is not parsed or executed.

Sourcetype sentence = {
  1. start : int;
  2. stop : int;
  3. synterp_state : Vernacstate.Synterp.t;
  4. scheduler_state_before : Scheduler.state;
  5. scheduler_state_after : Scheduler.state;
  6. ast : parsed_ast;
  7. id : Types.sentence_id;
}
Sourceval sentences : document -> sentence list
Sourceval sentences_sorted_by_loc : document -> sentence list
Sourceval get_sentence : document -> Types.sentence_id -> sentence option
Sourceval sentences_before : document -> int -> sentence list
Sourceval find_sentence : document -> int -> sentence option

find_sentence pos loc finds the sentence containing the loc

Sourceval find_sentence_before : document -> int -> sentence option

find_sentence_before pos loc finds the last sentence before the loc

Sourceval find_sentence_after : document -> int -> sentence option

find_sentence_after pos loc finds the first sentence after the loc

Sourceval find_next_qed : document -> int -> sentence option

find_next_qed parsed loc finds the next proof end

Sourceval get_first_sentence : document -> sentence option

get_first_sentence doc returns the first parsed sentence

Sourceval get_last_sentence : document -> sentence option

get_last_sentence doc returns the last parsed sentence

Sourceval range_of_id : document -> Stateid.t -> Lsp.Types.Range.t
Sourcemodule Internal : sig ... end