package coq-lsp

You can search for identifiers within the package.

in-package search v0.2.0

coq-lsp.coq
- Coq
  - Args
  - Ast
    
    Id
    
    Map
    
    Monad
    
    M
    
    Smart
    
    Set
    
    Meta
    
    Command
    
    Require
  - Compat
    
    Ocaml_414
    
    In_channel
    
    Out_channel
    
    Result
    
    O
  - Files
  - Glob
    
    Info
  - Goals
  - Init
  - Interp
    
    Require
  - Library_file
    
    Entry
  - Limits
    
    Coq
    
    Token
    
    Intf
    
    Token
    
    Mp
    
    Token
    
    Token
  - Limits_mp_impl
    
    Token
  - Loader
  - Message
  - Parsing
    
    Parsable
  - Print
  - Protect
    
    E
    
    O
    
    Error
    
    R
  - Save
  - State
    
    Proof
  - Utils
  - Workspace
    
    CmdLine
    
    Flags
    
    Require
    
    Warning
coq-lsp.fleche
- Fleche
  - Config
    
    Unicode_completion
  - Contents
    
    R
  - Debug
  - Doc
    
    Completion
    
    Env
    
    Node
    
    Ast
    
    Info
    
    Message
    
    Target
  - Info
    
    Completion
    
    Goals
    
    LC
    
    LineCol
    
    O
    
    Offset
    
    Point
    
    S
    
    P
  - Io
    
    CallBack
    
    Level
    
    Log
    
    Report
  - Memo
    
    Admit
    
    GlobalCacheStats
    
    Init
    
    Interp
    
    Require
    
    S
    
    Stats
  - Perf
    
    Info
    
    Sentence
  - Perf_analysis
  - Progress
    
    Info
  - ServerInfo
    
    Status
    
    Version
  - Stats
    
    Global
    
    Kind
  - Theory
    
    Check
    
    Register
    
    Completed
    
    InjectRequire
    
    Request
  - Version
coq-lsp.fleche.waterproof
- Fleche_waterproof
  - Json
    
    CAst
  - Ljson
  - Tjson
coq-lsp.lang
- Lang
  - Ast
    
    Info
    
    Name
  - Diagnostic
    
    Data
    
    Severity
  - LUri
    
    File
  - Point
  - Range
  - Utf
    
    Encoding
  - With_range
coq-lsp.lsp
- Lsp
coq-lsp.petanque
- Petanque
  - Agent
    
    Env
    
    Error
    
    Premise
    
    R
    
    Run_result
    
    State
coq-lsp.petanque.json
- Petanque_json
  - Client
    
    Chans
    
    S
    
    C
  - Interp
  - JAgent
    
    Env
    
    Error
    
    Goals
    
    Lang
    
    Range
    
    Premise
    
    R
    
    Run_result
    
    State
    
    Stdlib
    
    Result
  - Obj_map
    
    Make
    
    O
    
    Obj
    
    S
  - Protocol
    
    Goals
    
    Handler
    
    Params
    
    Params
    
    Response
    
    Handler
    
    Params
    
    Response
    
    Init
    
    Handler
    
    Response
    
    Params
    
    Response
    
    Message
    
    Params
    
    Notification
    
    S
    
    Params
    
    Premises
    
    Handler
    
    Params
    
    Params
    
    Response
    
    Request
    
    S
    
    Handler
    
    Params
    
    Response
    
    Params
    
    Response
    
    RunTac
    
    Handler
    
    Params
    
    Response
    
    Params
    
    Response
    
    Start
    
    Handler
    
    Params
    
    Response
    
    Params
    
    Response
    
    Trace
    
    Params
  - Utils
coq-lsp.plugin.astdump
- Astdump_plugin
  - Main
coq-lsp.plugin.example
- Example_plugin
  - Main
coq-lsp.plugin.goaldump
- Goaldumpl_plugin
  - Main
coq-lsp.plugin.save_vo
- Savevo_plugin
  - Main

Legend:
Library
Module
Module type
Parameter
Class
Class type

This module provides facilities for translating language-based locations to protocol-based locations.

After a long discussion (thanks Léo !), we have decided that the best is to have `Lang.Point` to store columns offset in the values that are native to the protocol under consideration, set by the upper layers.

This scheme kind of follows what we have done since the start with coq-lsp.

module Encoding : sig ... end

Future work: support setting protocol enconding

Unicode terminology refresher:

character, code point: The real unicode character
byte or 16bit offset / code unit: The encoded version

type utf8_string = string

type char = int

type utf8_index = int

type utf16_index = int

val utf16_offset_of_utf8_offset : 
  line:utf8_string ->
  offset:utf8_index ->
  utf16_index

UTF-16 offset from UTF-8 offset; line is enconded in UTF-8

val utf8_offset_of_utf16_offset : 
  line:utf8_string ->
  offset:utf16_index ->
  utf8_index

Get the byte position of a code point indexed in UTF-16 code units in a UTF-8 encoded utf8_string. Returns the position of the last character if the UTF-16 position was out of bounds.

To UTF-16 offsets

val length_utf16 : utf8_string -> utf16_index

Length in UTF-16 code points

Not used anywhere, remove?

val length : utf8_string -> char

Number of characters in the utf-8-encoded utf8_string.

Converstion from char to UTF-8/16

val utf8_offset_of_char : line:utf8_string -> char:char -> utf8_index option

UTF-8 Char to byte index position; line is enconded in UTF-8

val utf16_offset_of_char : line:utf8_string -> char:int -> utf16_index

Get the utf16 position of a code point indexed in unicode code points in a UTF-8 encoded utf8_string. The position must be in bounds.

Converstion to char from UTF-8/16

val char_of_utf8_offset : line:utf8_string -> offset:utf8_index -> char option

Byte index to character position also called a codepoint, line is encoded in UTF-8

val char_of_utf16_offset : line:utf8_string -> offset:utf16_index -> char

Get the unicode position of a code point indexed in UTF-16 code units in a utf-8 encoded utf8_string. Returns the position of the last character if the utf-16 position was out of bounds.

val next : string -> int -> int

For testing