package vscoq-language-server

You can search for identifiers within the package.

in-package search v0.2.0

vscoq-language-server
- Library vscoq-language-server.dm
  - Dm
    
    CompletionItems
    
    CompletionSuggester
    
    DelegationManager
    
    Job
    
    Worker
    
    MakeWorker
    
    Document
    
    Internal
    
    DocumentManager
    
    Internal
    
    ExecutionManager
    
    ProofWorkerProcess
    
    Log
    
    ParTactic
    
    TacticWorkerProcess
    
    PriorityManager
    
    RawDocument
    
    Scheduler
    
    SearchQuery
    
    Types
    
    Quickfix
- Library vscoq-language-server.language
  - Language
    
    Hover
- Library vscoq-language-server.lsp
  - Protocol
    
    ExtProtocol
    
    Notification
    
    Client
    
    InterpretToPointParams
    
    InterpretToEndParams
    
    StepBackwardParams
    
    StepForwardParams
    
    Server
    
    MoveCursorParams
    
    BlockOnErrorParams
    
    ProofViewParams
    
    CoqLogMessageParams
    
    Request
    
    Client
    
    ResetParams
    
    AboutParams
    
    CheckParams
    
    LocateParams
    
    PrintParams
    
    SearchParams
    
    DocumentStateParams
    
    DocumentStateResult
    
    LspWrapper
    
    Position
    
    Range
    
    QuickFixData
    
    DiagnosticSeverity
    
    FeedbackChannel
    
    CoqFeedback
    
    Printing
    
    ProofState
    
    Settings
    
    DelegationMode
    
    Mode
    
    Memory
    
    Proof
    
    Goals
    
    Messages
    
    Diff
    
    Mode
    
    Completion
    
    RankingAlgoritm
    
    Diagnostics
- Sources
  - vscoq-language-server.dm
    
    completionItems.ml
    
    completionSuggester.ml
    
    delegationManager.ml
    
    dm.ml
    
    document.ml
    
    documentManager.ml
    
    executionManager.ml
    
    log.ml
    
    parTactic.ml
    
    priorityManager.ml
    
    rawDocument.ml
    
    scheduler.ml
    
    searchQuery.ml
    
    types.ml
  - vscoq-language-server.language
    
    hover.ml
    
    language.ml
  - vscoq-language-server.lsp
    
    extProtocol.ml
    
    lspWrapper.ml
    
    printing.ml
    
    proofState.ml
    
    protocol.ml
    
    settings.ml

Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module `Dm.Document`Source

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 =

| TheoremKind of Decls.theorem_kind
| DefinitionType of Decls.definition_object_kind
| Other

Sourcetype outline_element = {

id : Types.sentence_id;
name : string;
type_ : proof_block_type;
statement : string;
range : Lsp.Types.Range.t;

}

Sourcetype outline = outline_element 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.

Source

val 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 = {

ast : Synterp.vernac_control_entry;
classification : Vernacextend.vernac_classification;
tokens : Tok.t list;

}

Sourcetype parsing_error = {

start : int;
stop : int;
msg : string Loc.located;
qf : Types.Quickfix.t list option;

}

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.

Sourcetype 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;

}

Sourcetype comment = {

start : int;
stop : int;
content : string;

}

Sourcetype code_line =

| Sentence of sentence
| ParsingError of parsing_error
| 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 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 schedule : document -> Scheduler.schedule

Sourceval range_of_id : document -> Stateid.t -> Lsp.Types.Range.t

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 -> Stateid.t -> 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)

Sourcemodule Internal : sig ... end

package vscoq-language-server

Module Dm.DocumentSource

Module `Dm.Document`Source