package vscoq-language-server
Install
Dune Dependency
Authors
Maintainers
Sources
md5=f528c1760966ac10d48b5f1c5531411a
sha512=1f69538ae5f78854b34e3f1a9d408714843e899bb96d063c2bfac410339b6a13ee5f30d5e7b3cd2bbd673169bcfdb550153ba741092cdc3ee3a8ca6446cc2240
doc/vscoq-language-server.dm/Dm/Document/index.html
Module Dm.Document
Source
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;
proof : proof_step list;
range : Lsp.Types.Range.t;
}
type parsing_end_info = {
unchanged_id : Types.sentence_id option;
invalid_ids : Types.sentence_id_set;
previous_document : document;
parsed_document : document;
}
create_document init_synterp_state text
creates a fresh document with content defined by text
under init_synterp_state
.
validate_document doc
triggers the parsing of the document line by line without launching any execution.
handle_event dpc ev
handles a parsing event for the document. One parsing event parses one line and prepares the next parsing event. Finally once the full parsing is done, the final event returs the id of the bottomost 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;
}
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 : sentence_state;
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)