package vscoq-language-server

  1. Overview
  2. Docs
VSCoq language server

Install

Dune Dependency

Authors

Maintainers

Sources

vscoq-language-server-2.0.3-coq8.18.tar.gz
md5=37688b8df4ccfc920a57552d0ebc0d3a
sha512=0db05bdfc4409cf8e5a43d191220b4ebd47978bcbb6fd41075ee745dd448b75e98677c81657809c30627c875e5fd54fbef180e6d30cb0a8e56ca26cbf8c5adb8

doc/src/vscoq-language-server.lsp/lspWrapper.ml.html

Source file lspWrapper.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
(**************************************************************************)
(*                                                                        *)
(*                                 VSCoq                                  *)
(*                                                                        *)
(*                   Copyright INRIA and contributors                     *)
(*       (see version control and README file for authors & dates)        *)
(*                                                                        *)
(**************************************************************************)
(*                                                                        *)
(*   This file is distributed under the terms of the MIT License.         *)
(*   See LICENSE file.                                                    *)
(*                                                                        *)
(**************************************************************************)
open Lsp.Types
open Sexplib.Std
open Printing

module Position = struct

  include Lsp.Types.Position

  type t = [%import: Lsp.Types.Position.t] [@@deriving sexp]
 
  let compare pos1 pos2 =
    match Int.compare pos1.line pos2.line with
    | 0 -> Int.compare pos1.character pos2.character
    | x -> x

  let to_string pos = Format.sprintf "(%i,%i)" pos.line pos.character

end

module Range = struct

  include Lsp.Types.Range

  type t = [%import: Lsp.Types.Range.t] [@@deriving sexp]

  let included ~in_ { start; end_ } =
    let (<=) x y = Position.compare x y <= 0 in
    in_.start <= start && end_ <= in_.end_

end 

module DiagnosticSeverity = struct

  type t = [%import: Lsp.Types.DiagnosticSeverity.t] [@@deriving sexp]

  let yojson_of_t v = Lsp.Types.DiagnosticSeverity.yojson_of_t v
  let t_of_yojson v = Lsp.Types.DiagnosticSeverity.t_of_yojson v

  let of_feedback_level = let open DiagnosticSeverity in function
    | Feedback.Error -> Error
    | Feedback.Warning -> Warning
    | Feedback.(Info | Debug | Notice) -> Information

end

type query_result =
  { id : string;
    name : pp;
    statement : pp;
  } [@@deriving yojson]

type notification =
  | QueryResultNotification of query_result
OCaml

Innovation. Community. Security.