package coq-lsp

You can search for identifiers within the package.

in-package search v0.2.0

Language Server Protocol native server for Coq

Install

dune-project

Dependency

github.com Readme Changelog Edit opam file Versions (36)

Authors

Maintainers

E

e@x80.org

Sources

coq-lsp-0.2.5+9.1.tbz

sha256=488520e2720cd0601a623be39ff87223d81ca1d2f81c77641f803fda21f3717e

sha512=146e43a6a9c516f4e7fe143d4fdf3e1e7ecdcd73ea5cc3e09b2886f68aa05210c016e905bf1596341faa0b55709ad530ef86212c92790b6dce6050a0a00e3325

doc/src/coq-lsp.lsp/jLang.ml.html

Source file `jLang.ml`

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
(************************************************************************)
(* Coq Language Server Protocol                                         *)
(* Copyright 2019 MINES ParisTech -- LGPL 2.1+                          *)
(* Copyright 2019-2023 Inria -- LGPL 2.1+                               *)
(* Written by: Emilio J. Gallego Arias                                  *)
(************************************************************************)

module Pp_t = JCoq.Pp_t

module Point = struct
  type t = [%import: Lang.Point.t] [@@deriving yojson]

  module Mode = struct
    type t =
      | LineColumn
          (** Points are standard LSP objects with [line] [character] field;
              this is the default *)
      | Offset  (** Points are objects with only the [offset] *)
      | Full
          (** Points include / require [line], [character], and [offset] field *)

    (** Set the mode for serialization. *)
    let default = ref LineColumn

    let set v = default := v
  end

  module PointLC = struct
    type t =
      { line : int
      ; character : int
      }
    [@@deriving yojson]

    let conv { Lang.Point.line; character; offset = _ } = { line; character }
    let vnoc { line; character } = { Lang.Point.line; character; offset = -1 }
  end

  module PointOffset = struct
    type t = { offset : int } [@@deriving yojson]

    let conv { Lang.Point.line = _; character = _; offset } = { offset }
    let vnoc { offset } = { Lang.Point.line = -1; character = -1; offset }
  end

  let of_yojson json =
    let open Ppx_deriving_yojson_runtime in
    match !Mode.default with
    | LineColumn -> PointLC.(of_yojson json >|= vnoc)
    | Offset -> PointOffset.(of_yojson json >|= vnoc)
    | Full -> of_yojson json

  let to_yojson p =
    match !Mode.default with
    | LineColumn -> PointLC.(to_yojson (conv p))
    | Offset -> PointOffset.(to_yojson (conv p))
    | Full -> to_yojson p
end

module Range = struct
  type t = [%import: (Lang.Range.t[@with Lang.Point.t := Point.t])]
  [@@deriving yojson]
end

module LUri = struct
  module File = struct
    type t = Lang.LUri.File.t

    let to_yojson uri = `String (Lang.LUri.File.to_string_uri uri)

    let invalid_uri msg obj =
      let msg =
        Format.asprintf "@[%s@] for object: @[%a@]" msg Yojson.Safe.pp obj
      in
      Error msg

    let of_yojson uri =
      match uri with
      | `String uri as obj -> (
        let uri = Lang.LUri.of_string uri in
        match Lang.LUri.File.of_uri uri with
        | Result.Ok t -> Result.Ok t
        | Result.Error msg -> invalid_uri ("failed to parse uri: " ^ msg) obj)
      | obj -> invalid_uri "expected uri string, got json object" obj
  end
end

module Qf = struct
  type 'l t = [%import: 'l Lang.Qf.t] [@@deriving yojson]
end

module Diagnostic = struct
  module QualId = struct
    type t = [%import: Lang.Diagnostic.QualId.t] [@@deriving yojson]
  end

  module FailedRequire = struct
    type t = [%import: Lang.Diagnostic.FailedRequire.t] [@@deriving yojson]
  end

  module Data = struct
    type t =
      [%import:
        (Lang.Diagnostic.Data.t
        [@with
          Lang.Qf.t := Qf.t;
          Lang.Range.t := Range.t])]
    [@@deriving yojson]
  end

  module Severity = struct
    type t = [%import: Lang.Diagnostic.Severity.t] [@@deriving yojson]
  end

  type t = [%import: ('a Lang.Diagnostic.t[@with Lang.Range.t := Range.t])]
  [@@deriving yojson]
end

module Stdlib = JStdlib

module With_range = struct
  type 'a t = [%import: ('a Lang.With_range.t[@with Lang.Range.t := Range.t])]
  [@@deriving yojson]
end

module Ast = struct
  module Name = struct
    type t = [%import: Lang.Ast.Name.t] [@@deriving yojson]
  end

  module Info = struct
    type t =
      [%import:
        (Lang.Ast.Info.t
        [@with
          Lang.Range.t := Range.t;
          Lang.With_range.t := With_range.t])]
    [@@deriving yojson]
  end
end