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

Sourcetype proof_block_type =
  1. | TheoremKind
  2. | DefinitionType
  3. | InductiveType
  4. | BeginSection
  5. | BeginModule
  6. | End
  7. | Other
Sourcetype proof_step = {
  1. id : Types.sentence_id;
  2. tactic : string;
  3. range : Lsp.Types.Range.t;
}
Sourcetype outline_element = {
  1. id : Types.sentence_id;
  2. name : string;
  3. type_ : proof_block_type;
  4. statement : string;
  5. proof : proof_step list;
  6. range : Lsp.Types.Range.t;
}
Sourcetype outline = outline_element list
Sourcetype parsing_end_info = {
  1. unchanged_id : Types.sentence_id option;
  2. invalid_ids : Types.sentence_id_set;
  3. previous_document : document;
  4. parsed_document : document;
}
Sourcetype event
Sourceval pp_event : Format.formatter -> event -> unit
Sourcetype events = event Sel.Event.t list
Sourceval raw_document : document -> RawDocument.t
Sourceval outline : document -> outline
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 -> document * events

validate_document doc triggers the parsing of the document line by line without launching any execution.

Sourceval handle_event : document -> event -> document * events * parsing_end_info option

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.

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 : Pp.t Loc.located;
  4. qf : Types.Quickfix.t list option;
  5. str : string;
}
Sourcetype parse_state
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_edit : document -> Types.text_edit -> document

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.

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.

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

Sourcetype sentence_state =
  1. | Error of parsing_error
  2. | Parsed of parsed_ast
Sourcetype sentence = {
  1. parsing_start : int;
  2. start : int;
  3. stop : int;
  4. synterp_state : Vernacstate.Synterp.t;
  5. scheduler_state_before : Scheduler.state;
  6. scheduler_state_after : Scheduler.state;
  7. ast : sentence_state;
  8. id : Types.sentence_id;
  9. messages : Types.feedback_message list;
  10. checked : Types.sentence_checking_result option;
}
Sourcetype comment = {
  1. start : int;
  2. stop : int;
  3. content : string;
}
Sourcetype code_line =
  1. | Sentence of sentence
  2. | ParsingError of parsing_error
  3. | Comment of comment
Sourceval sentences : document -> sentence list
Sourceval code_lines_sorted_by_loc : document -> code_line list
Sourceval code_lines_by_end_sorted_by_loc : document -> code_line 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 doc loc finds the sentence containing the loc

Sourceval find_sentence_before : document -> int -> sentence option

find_sentence_before doc loc finds the last sentence before the loc

Sourceval find_sentence_before_pos : document -> Lsp.Types.Position.t -> sentence option

find_sentence_before_pos doc pos finds the sentence before the pos

Sourceval find_sentence_after : document -> int -> sentence option

find_sentence_after doc loc finds the first sentence after the loc

Sourceval find_sentence_after_pos : document -> Lsp.Types.Position.t -> sentence option

find_sentence_after_pos doc pos finds the first sentence after the pos

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 is_sentence_above : document -> Types.sentence_id -> Types.sentence_id -> bool

is_sentence_above doc id1 id2 check is id1 is above id2

Sourceval has_sentence : document -> Types.sentence_id -> bool

has_sentence doc id tells if id is in the document

range_of_id doc id returns a Range object coressponding to the sentence id given in argument

Sourceval range_of_id_with_blank_space : document -> Types.sentence_id -> Lsp.Types.Range.t

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)

all_feedback doc returns all sentences with a feedback

feedback doc id returns all feedback messages for id

Sourceval all_checking_errors : document -> (Types.sentence_id * (Loc.t option * Pp.t * Types.Quickfix.t list option)) list

all_checking_errors doc returns all sentences that were checked and resulted in an error

Sourceval error : document -> Types.sentence_id -> (Loc.t option * Pp.t * Types.Quickfix.t list option) option

error doc id returns the checking error for id, if any

append_feedback doc id msg appends msg to existing messages on id

Sourceval shift_feedbacks_and_checking_errors : start:int -> offset:int -> document -> document

shift_feedbacks_and_checking_errors ~start ~stop doc shifts all messages past start by offset

update_checked doc id v updates the checked field of sentence id

Sourceval set_unchecked : document -> Types.sentence_id -> document

remove_checked doc id marks id as unchecked

Sourceval is_checked : document -> Types.sentence_id -> bool

is_checked doc id tells if id is checked

Sourcemodule Internal : sig ... end