package vscoq-language-server
Install
Dune Dependency
Authors
Maintainers
Sources
md5=81c195fcbe9b23c26db9704a0b8e37f8
sha512=9b175796b231e3663b1cdd546fde898c1d19a6a4eb16671970797045e0e29acc008630634f0d15fa34a94ccc14a0c16d3851efbf0b74f3e1ac6ada1f1461f7e1
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).
The document gathers the text, which is partially validated (parsed into sentences
type outline_element = {id : Types.sentence_id;name : string;type_ : proof_block_type;statement : string;range : Lsp.Types.Range.t;
}create_document init_synterp_state text creates a fresh document with content defined by text under init_synterp_state.
val validate_document :
document ->
Types.sentence_id option * Types.sentence_id_set * documentvalidate_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
type parsed_ast = {ast : Synterp.vernac_control_entry;classification : Vernacextend.vernac_classification;tokens : Tok.t list;
}type parsing_error = {start : int;stop : int;msg : string Loc.located;qf : Types.Quickfix.t list option;
}parse_errors doc returns the list of sentences which failed to parse (see validate_document) together with their error message
parse_errors doc returns the list of sentences which failed to parse (see validate_document) together with their error message
apply_text_edits doc edits updates the text of doc with edits. The new text is not parsed or executed.
apply_text_edits doc edits updates the text of doc with edits. The new text is not parsed or executed.
apply_text_edits doc edits updates the text of doc with edits. The new text is not parsed or executed.
type sentence = {parsing_start : int;start : int;stop : int;synterp_state : Vernacstate.Synterp.t;scheduler_state_before : Scheduler.state;scheduler_state_after : Scheduler.state;ast : parsed_ast;id : Types.sentence_id;
}find_sentence pos loc finds the sentence containing the loc
find_sentence_before pos loc finds the last sentence before the loc
find_sentence_after pos loc finds the first sentence after the loc
find_next_qed parsed loc finds the next proof end
get_first_sentence doc returns the first parsed sentence
get_last_sentence doc returns the last parsed sentence
range_of_id doc id returns a Range object coressponding to the sentence id given in argument
range_of_id_with_blank_space doc id returns a Range object coressponding to the sentence id given in argument but with the white spaces before (until the previous sentence)