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
    
    PointInterpretationMode
    
    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.ExecutionManager`Source

The event manager is in charge of the actual event of tasks (as defined by the scheduler), caching event states and invalidating them. It can delegate to worker processes via DelegationManager

Sourcetype delegation_mode =

| CheckProofsInMaster
| SkipProofs
| DelegateProofsToWorkers of {
1. number_of_workers : int;
}

Sourcetype options = {

delegation_mode : delegation_mode;
completion_options : Protocol.Settings.Completion.t;
enableDiagnostics : bool;

}

Sourceval is_diagnostics_enabled : unit -> bool

Sourcetype state

Execution state, includes the cache

Sourcetype event

Sourcetype events = event Sel.Event.t list

Sourcetype errored_sentence = Types.sentence_id option

Source

type feedback_message =
  Feedback.level * Loc.t option * Types.Quickfix.t list * Pp.t

Sourceval pr_event : event -> Pp.t

Sourceval init : Vernacstate.t -> state * event Sel.Event.t

Sourceval destroy : state -> unit

Sourceval get_options : unit -> options

Sourceval set_options : options -> unit

Sourceval set_default_options : unit -> unit

Source

val invalidate : 
  Document.document ->
  Scheduler.schedule ->
  Types.sentence_id ->
  state ->
  state

Sourceval error : state -> Types.sentence_id -> (Loc.t option * Pp.t) option

Sourceval feedback : state -> Types.sentence_id -> feedback_message list

Source

val all_errors : 
  state ->
  (Types.sentence_id * (Loc.t option * Pp.t * Types.Quickfix.t list option))
    list

Sourceval all_feedback : state -> (Types.sentence_id * feedback_message) list

Source

val shift_overview : 
  state ->
  before:RawDocument.t ->
  after:RawDocument.t ->
  start:int ->
  offset:int ->
  state

Sourceval shift_diagnostics_locs : state -> start:int -> offset:int -> state

Sourceval executed_ids : state -> Types.sentence_id list

Sourceval is_executed : state -> Types.sentence_id -> bool

Sourceval is_remotely_executed : state -> Types.sentence_id -> bool

Source

val get_context : 
  state ->
  Types.sentence_id ->
  (Evd.evar_map * Environ.env) option

Sourceval get_initial_context : state -> Evd.evar_map * Environ.env

Sourceval get_vernac_state : state -> Types.sentence_id -> Vernacstate.t option

Returns the vernac state after the sentence

Source

val handle_event : 
  event ->
  state ->
  Types.sentence_id option * state option * events

Events for the main loop

Sourcetype prepared_task

Execution happens in two steps. In particular the event one takes only one task at a time to ease checking for interruption

Source

val build_tasks_for : 
  Document.document ->
  Scheduler.schedule ->
  state ->
  Types.sentence_id ->
  bool ->
  Vernacstate.t * prepared_task list * state * Types.sentence_id option

Source

val execute : 
  state ->
  (Vernacstate.t * events * bool) ->
  prepared_task ->
  state * Vernacstate.t * events * bool * errored_sentence

Source

val update_overview : 
  prepared_task ->
  prepared_task list ->
  state ->
  Document.document ->
  state

Sourceval cut_overview : prepared_task -> state -> Document.document -> state

Sourceval update_processed : Types.sentence_id -> state -> Document.document -> state

Sourceval prepare_overview : state -> Protocol.LspWrapper.Range.t list -> state

Sourceval overview : state -> Types.exec_overview

Source

val overview_until_range : 
  state ->
  Protocol.LspWrapper.Range.t ->
  Types.exec_overview

Sourceval print_exec_overview_of_state : state -> unit

Sourcemodule ProofWorkerProcess : sig ... end

Coq toplevels for delegation without fork

package vscoq-language-server

Module Dm.ExecutionManagerSource

Module `Dm.ExecutionManager`Source