package coq-lsp

You can search for identifiers within the package.

in-package search v0.2.0

package coq-lsp

coq-lsp
- Library Astdump_plugin
  - Astdump_plugin
    
    Main
- Library Example_plugin
  - Example_plugin
    
    Main
- Library Goaldumpl_plugin
  - Goaldumpl_plugin
    
    Main
- Library Savevo_plugin
  - Savevo_plugin
    
    Main
- Library coq-lsp.coq
  - Coq
    
    Args
    
    Ast
    
    Id
    
    Set
    
    Map
    
    Require
    
    Meta
    
    Command
    
    Compat
    
    Ocaml_414
    
    In_channel
    
    Out_channel
    
    Result
    
    O
    
    Files
    
    Glob
    
    Info
    
    Goals
    
    Init
    
    Interp
    
    Require
    
    Library_file
    
    Entry
    
    Limits
    
    Intf
    
    Token
    
    Coq
    
    Token
    
    Mp
    
    Token
    
    Token
    
    Limits_mp_impl
    
    Token
    
    Loader
    
    Message
    
    Parsing
    
    Parsable
    
    Print
    
    Protect
    
    Error
    
    R
    
    E
    
    O
    
    Save
    
    State
    
    Proof
    
    Declare
    
    OblState
    
    View
    
    Obl
    
    Utils
    
    Workspace
    
    Flags
    
    Warning
    
    Require
    
    CmdLine
- Library coq-lsp.fleche
  - Fleche
    
    Config
    
    Unicode_completion
    
    Contents
    
    R
    
    Debug
    
    Doc
    
    Node
    
    Ast
    
    Info
    
    Message
    
    Completion
    
    Env
    
    Target
    
    Info
    
    Point
    
    LineCol
    
    Offset
    
    S
    
    P
    
    LC
    
    O
    
    Goals
    
    Completion
    
    Io
    
    Level
    
    CallBack
    
    Log
    
    Report
    
    Memo
    
    Stats
    
    S
    
    Init
    
    Interp
    
    Require
    
    Admit
    
    GlobalCacheStats
    
    Perf
    
    Info
    
    Sentence
    
    Perf_analysis
    
    Progress
    
    Info
    
    ServerInfo
    
    Version
    
    Status
    
    Stats
    
    Kind
    
    Global
    
    Theory
    
    Check
    
    Request
    
    Register
    
    InjectRequire
    
    Completed
    
    Version
- Library coq-lsp.lang
  - Lang
    
    Ast
    
    Name
    
    Info
    
    Diagnostic
    
    Data
    
    Severity
    
    LUri
    
    File
    
    Point
    
    Range
    
    Utf
    
    Encoding
    
    With_range
- Library coq-lsp.lsp
  - Lsp
    
    Base
    
    Params
    
    Notification
    
    Request
    
    Response
    
    Message
    
    ProgressToken
    
    ProgressParams
    
    WorkDoneProgressBegin
    
    WorkDoneProgressReport
    
    WorkDoneProgressEnd
    
    Core
    
    Location
    
    LocationLink
    
    DocumentSymbol
    
    SymInfo
    
    HoverContents
    
    HoverInfo
    
    LabelDetails
    
    TextEditReplace
    
    CompletionData
    
    Command
    
    CodeLens
    
    SelectionRange
    
    DocumentDiagnosticParams
    
    FullDocumentDiagnosticReport
    
    UnchangedDocumentDiagnosticReport
    
    DocumentDiagnosticReportPartialResult
    
    Doc
    
    TextDocumentItem
    
    TextDocumentIdentifier
    
    OVersionedTextDocumentIdentifier
    
    VersionedTextDocumentIdentifier
    
    Io
    
    TraceValue
    
    Lvl
    
    JCoq
    
    Loc
    
    Names
    
    Evar
    
    Evar_kinds
    
    Pp
    
    Goals
    
    Goals_
    
    Ast
    
    Declare
    
    OblState
    
    View
    
    Obl
    
    JFleche
    
    Config
    
    FileProgress
    
    Message
    
    GoalsAnswer
    
    CompletionStatus
    
    RangedSpan
    
    FlecheDocument
    
    SentencePerfData
    
    DocumentPerfData
    
    JLang
    
    Point
    
    Range
    
    LUri
    
    File
    
    Diagnostic
    
    Point
    
    Range
    
    Workspace
    
    WorkspaceFolder
    
    WorkspaceFoldersChangeEvent
    
    DidChangeWorkspaceFoldersParams
- Library coq-lsp.petanque
  - Petanque
    
    Agent
    
    State
    
    Env
    
    Error
    
    R
    
    Run_result
    
    Premise
- Library fleche_waterproof
  - Fleche_waterproof
    
    Json
    
    CAst
    
    Ljson
    
    Tjson
- Library petanque_json
  - Petanque_json
    
    Client
    
    Chans
    
    S
    
    Interp
    
    A
    
    JAgent
    
    State
    
    Env
    
    Stdlib
    
    Result
    
    Result
    
    Error
    
    Run_result
    
    R
    
    Goals
    
    Lang
    
    Range
    
    Premise
    
    Obj_map
    
    Obj
    
    S
    
    Make
    
    Protocol
    
    Handler
    
    Params
    
    Response
    
    Request
    
    S
    
    Params
    
    Response
    
    Handler
    
    Params
    
    Response
    
    Init
    
    Params
    
    Response
    
    Handler
    
    Params
    
    Response
    
    Start
    
    Params
    
    Response
    
    Handler
    
    Params
    
    Response
    
    RunTac
    
    Params
    
    Response
    
    Handler
    
    Params
    
    Response
    
    Goals
    
    Params
    
    Response
    
    Handler
    
    Params
    
    Response
    
    Premises
    
    Params
    
    Response
    
    Handler
    
    Params
    
    Response
    
    Notification
    
    S
    
    Params
    
    Trace
    
    Params
    
    Message
    
    Params
    
    Utils
- Sources
  - Astdump_plugin
    
    astdump_plugin.ml
    
    main.ml
  - Example_plugin
    
    example_plugin.ml
    
    main.ml
  - Goaldumpl_plugin
    
    goaldumpl_plugin.ml
    
    main.ml
  - Savevo_plugin
    
    main.ml
    
    savevo_plugin.ml
  - coq-lsp.coq
    
    args.ml
    
    ast.ml
    
    compat.ml
    
    coq.ml
    
    files.ml
    
    glob.ml
    
    goals.ml
    
    init.ml
    
    interp.ml
    
    library_file.ml
    
    limits.ml
    
    limits_mp_impl.ml
    
    loader.ml
    
    message.ml
    
    parsing.ml
    
    print.ml
    
    protect.ml
    
    save.ml
    
    state.ml
    
    utils.ml
    
    workspace.ml
  - coq-lsp.fleche
    
    config.ml
    
    contents.ml
    
    debug.ml
    
    doc.ml
    
    fleche.ml
    
    info.ml
    
    io.ml
    
    memo.ml
    
    perf.ml
    
    perf_analysis.ml
    
    progress.ml
    
    serverInfo.ml
    
    stats.ml
    
    theory.ml
    
    version.ml
  - coq-lsp.lang
    
    ast.ml
    
    diagnostic.ml
    
    lUri.ml
    
    lang.ml
    
    point.ml
    
    range.ml
    
    utf.ml
    
    with_range.ml
  - coq-lsp.lsp
    
    base.ml
    
    core.ml
    
    doc.ml
    
    io.ml
    
    jCoq.ml
    
    jFleche.ml
    
    jLang.ml
    
    lsp.ml
    
    workspace.ml
  - coq-lsp.petanque
    
    agent.ml
    
    petanque.ml
  - fleche_waterproof
    
    fleche_waterproof.ml
    
    json.ml
    
    ljson.ml
    
    tjson.ml
  - petanque_json
    
    client.ml
    
    interp.ml
    
    jAgent.ml
    
    obj_map.ml
    
    petanque_json.ml
    
    protocol.ml
    
    utils.ml

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

Module `Goals.Handler`Source

Sourcemodule Params : sig ... end

Sourcemodule Response = Response

Source

val handler : 
  token:Coq.Limits.Token.t ->
  Params.t ->
  string Coq.Goals.reified_pp option Petanque.Agent.R.t

package coq-lsp

Module Goals.HandlerSource

Module `Goals.Handler`Source