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
- Library vscoq-language-server.language
  - Language
    
    Hover
- Library vscoq-language-server.lsp
  - Protocol
    
    ExtProtocol
    
    Notification
    
    Client
    
    InterpretToPointParams
    
    InterpretToEndParams
    
    StepBackwardParams
    
    StepForwardParams
    
    Server
    
    MoveCursorParams
    
    ProofViewParams
    
    Request
    
    Client
    
    ResetParams
    
    AboutParams
    
    CheckParams
    
    LocateParams
    
    PrintParams
    
    SearchParams
    
    DocumentStateParams
    
    DocumentStateResult
    
    LspWrapper
    
    Position
    
    Range
    
    DiagnosticSeverity
    
    Printing
    
    ProofState
    
    Settings
    
    DelegationMode
    
    Mode
    
    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.DocumentManager`Source

The document manager holds the view that Coq has of the currently open states. It makes it easy for IDEs to handle text edits, navigate and get feedback. Note that it does not require IDEs to parse vernacular sentences.

Sourcetype observe_id =

| Id of Types.sentence_id
| Top

Sourcetype state

Sourcetype event

Sourceval pp_event : Format.formatter -> event -> unit

Sourcetype events = event Sel.Event.t list

Source

val init : 
  Vernacstate.t ->
  opts:Coqargs.injection_command list ->
  Lsp.Types.DocumentUri.t ->
  text:string ->
  observe_id option ->
  state * events

init st opts uri text initializes the document manager with initial vernac state st on which command line opts will be set.

Sourceval apply_text_edits : state -> Types.text_edit list -> state

apply_text_edits doc edits updates the text of doc with edits. The new document is parsed, outdated executions states are invalidated, and the observe id is updated.

Sourceval clear_observe_id : state -> state

clear_observe_id state updates the state to make the observe_id None

Sourceval reset_to_top : state -> state

reset_to_top state updates the state to make the observe_id Top

Source

val get_next_range : 
  state ->
  Protocol.LspWrapper.Position.t ->
  Protocol.LspWrapper.Range.t option

get_next_range st pos get the range of the next sentence relative to pos

Source

val get_previous_range : 
  state ->
  Protocol.LspWrapper.Position.t ->
  Protocol.LspWrapper.Range.t option

get_previous_pos st pos get the range of the previous sentence relative to pos

Source

val interpret_to_position : 
  state ->
  Protocol.LspWrapper.Position.t ->
  state * events

interpret_to_position stateful doc pos navigates to the last sentence ending before or at pos and returns the resulting state. The stateful flag determines if we record the resulting position in the state.

Sourceval interpret_to_previous : state -> state * events

interpret_to_previous doc navigates to the previous sentence in doc and returns the resulting state.

Sourceval interpret_to_next : state -> state * events

interpret_to_next doc navigates to the next sentence in doc and returns the resulting state.

Sourceval interpret_to_end : state -> state * events

interpret_to_end doc navigates to the last sentence in doc and returns the resulting state.

Sourceval interpret_in_background : state -> state * events

interpret_in_background doc same as interpret_to_end but computation is done in background (with lower priority)

Sourceval reset : state -> state * events

resets Coq

Sourceval executed_ranges : state -> Types.exec_overview

returns the ranges corresponding to the sentences that have been executed and remotely executes

Sourceval observe_id_range : state -> Protocol.LspWrapper.Range.t option

returns the range of the sentence referenced by observe_id *

Source

val get_messages : 
  state ->
  Protocol.LspWrapper.Position.t option ->
  (Protocol.LspWrapper.DiagnosticSeverity.t * Protocol.Printing.pp) list

Sourceval all_diagnostics : state -> Lsp.Types.Diagnostic.t list

all_diagnostics doc returns the diagnostics corresponding to the sentences that have been executed in doc.

Source

val get_proof : 
  state ->
  Protocol.Settings.Goals.Diff.Mode.t ->
  Protocol.LspWrapper.Position.t option ->
  Protocol.ProofState.t option

Source

val get_completions : 
  state ->
  Protocol.LspWrapper.Position.t ->
  (CompletionItems.completion_item list, string) Result.t

Sourceval handle_event : event -> state -> state option * events

handles events and returns a new state if it was updated

Source

val search : 
  state ->
  id:string ->
  Protocol.LspWrapper.Position.t ->
  string ->
  Protocol.LspWrapper.notification Sel.Event.t list

Source

val about : 
  state ->
  Protocol.LspWrapper.Position.t ->
  pattern:string ->
  (Protocol.Printing.pp, string) Result.t

Source

val hover : 
  state ->
  Protocol.LspWrapper.Position.t ->
  Lsp.Types.MarkupContent.t option

Returns an optional Result: if None, the position did not have a word, if Some, an Ok/Error result is returned.

Source

val check : 
  state ->
  Protocol.LspWrapper.Position.t ->
  pattern:string ->
  (Protocol.Printing.pp, string) Result.t

Source

val locate : 
  state ->
  Protocol.LspWrapper.Position.t ->
  pattern:string ->
  (Protocol.Printing.pp, string) Result.t

Source

val print : 
  state ->
  Protocol.LspWrapper.Position.t ->
  pattern:string ->
  (Protocol.Printing.pp, string) Result.t

Sourcemodule Internal : sig ... end

package vscoq-language-server

Module Dm.DocumentManagerSource

Module `Dm.DocumentManager`Source