package coq-lsp

You can search for identifiers within the package.

in-package search v0.2.0

package coq-lsp

coq-lsp.coq
- Coq
  - Ast
    
    Id
  - Goals
  - Init
  - Interp
  - Loader
  - Message
  - Parsing
    
    Parsable
  - Print
  - Protect
    
    E
    
    Error
    
    R
  - Save
  - State
    
    Proof
  - Utf8
  - Utils
  - Workspace
    
    CmdLine
    
    Flags
    
    Warning
coq-lsp.fleche
- Fleche
  - Config
    
    Unicode_completion
  - Contents
    
    R
  - Debug
  - Doc
    
    Completion
    
    Node
    
    Ast
    
    Info
    
    Message
    
    Target
  - Info
    
    Completion
    
    Goals
    
    LC
    
    LineCol
    
    O
    
    Offset
    
    Point
    
    S
    
    P
  - Io
    
    CallBack
    
    Log
    
    Report
  - Memo
    
    Admit
    
    CacheStats
    
    Init
    
    Interp
    
    Stats
  - Perf
    
    Sentence
  - Perf_analysis
  - Progress
    
    Info
  - Stats
    
    Kind
  - Theory
    
    Check
    
    Register
    
    Completed
    
    Request
  - Version
coq-lsp.fleche.waterproof
- Fleche_waterproof
  - Json
    
    CAst
  - Ljson
  - Tjson
coq-lsp.lang
- Lang
  - Ast
    
    Info
    
    Name
  - Diagnostic
    
    Extra
  - LUri
    
    File
  - Point
  - Range
  - With_range
coq-lsp.lsp
- Lsp
coq-lsp.plugin.example
- Example_plugin
  - Main

Legend:
Library
Module
Module type
Parameter
Class
Class type

module Node : sig ... end

module Completion : sig ... end

type t = private {

uri : Lang.LUri.File.t;
version : int;
contents : Contents.t;
toc : Lang.Range.t CString.Map.t;
root : Coq.State.t;
nodes : Node.t list;
diags_dirty : bool;
completed : Completion.t;

}

A Flèche document is basically a node list, which is a crude form of a meta-data map Range.t -> data, where for now data is the contents of Node.t.

val asts : t -> Node.Ast.t list

Return the list of all asts in the doc

val diags : t -> Lang.Diagnostic.t list

Return the list of all diags in the doc

val create : 
  state:Coq.State.t ->
  workspace:Coq.Workspace.t ->
  uri:Lang.LUri.File.t ->
  version:int ->
  raw:string ->
  (t, Loc.t) Coq.Protect.R.t

Create a new Coq document, this is cached!

val bump_version : version:int -> raw:string -> t -> t Contents.R.t

Update the contents of a document, updating the right structures for incremental checking.

module Target : sig ... end

Checking targets, this specifies what we expect check to reach

val check : io:Io.CallBack.t -> target:Target.t -> doc:t -> unit -> t

check ~io ~target ~doc (), check document doc, target will have Flèche stop after the point specified there has been reached. Output functions are in the io record, used to send partial updates.

val save : doc:t -> (unit, Loc.t) Coq.Protect.E.t

save ~doc will save doc .vo file. It will fail if proofs are open, or if the document completion status is not Yes

val create_failed_permanent : 
  state:Coq.State.t ->
  uri:Lang.LUri.File.t ->
  version:int ->
  raw:string ->
  t Contents.R.t

This is internal, to workaround the Coq multiple-docs problem