package coq-lsp

  1. Overview
  2. Docs
package coq-lsp
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file io.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
(************************************************************************)
(* Rocq Language Server Protocol                                        *)
(* Copyright 2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+      *)
(* Copyright 2019-2024 Inria      -- Dual License LGPL 2.1 / GPL3+      *)
(* Copyright 2024-2025 EJGA       -- Dual License LGPL 2.1 / GPL3+      *)
(* Written by: Emilio J. Gallego Arias                                  *)
(************************************************************************)

module Level = struct
  type t =
    | Error
    | Warning
    | Info
    | Log
    | Debug
end

module CallBack = struct
  type t =
    { trace : string -> ?verbose:string -> string -> unit
    ; message : lvl:Level.t -> message:string -> unit
    ; diagnostics :
        uri:Lang.LUri.File.t -> version:int -> Lang.Diagnostic.t list -> unit
    ; fileProgress :
        uri:Lang.LUri.File.t -> version:int -> Progress.Info.t list -> unit
    ; perfData : uri:Lang.LUri.File.t -> version:int -> Perf.t -> unit
    ; serverVersion : ServerInfo.Version.t -> unit
    ; serverStatus : ServerInfo.Status.t -> unit
    }

  let default =
    { trace = (fun _ ?verbose:_ _ -> ())
    ; message = (fun ~lvl:_ ~message:_ -> ())
    ; diagnostics = (fun ~uri:_ ~version:_ _ -> ())
    ; fileProgress = (fun ~uri:_ ~version:_ _ -> ())
    ; perfData = (fun ~uri:_ ~version:_ _ -> ())
    ; serverVersion = (fun _ -> ())
    ; serverStatus = (fun _ -> ())
    }

  let cb = ref default
  let set t = cb := t
end

(** Trace *)
module TraceValue = struct
  type t =
    | Off
    | Messages
    | Verbose

  let of_string = function
    | "messages" -> Ok Messages
    | "verbose" -> Ok Verbose
    | "off" -> Ok Off
    | v -> Error ("TraceValue.parse: " ^ v)

  let to_string = function
    | Off -> "off"
    | Messages -> "messages"
    | Verbose -> "verbose"
end

module Log = struct
  let trace_value = ref TraceValue.Off
  let set_trace_value value = trace_value := value

  let trace_ d ?verbose m =
    match !trace_value with
    | Off -> ()
    | Messages -> !CallBack.cb.trace d ?verbose:None m
    | Verbose -> !CallBack.cb.trace d ?verbose m

  let trace d ?verbose = Format.kasprintf (fun m -> trace_ d ?verbose m)

  let trace_object hdr obj =
    (* Fixme, use the extra parameter *)
    trace hdr "[%s]: @[%a@]" hdr Yojson.Safe.(pretty_print ~std:false) obj

  let feedback part feedback =
    if not (CList.is_empty feedback) then
      (* Put feedbacks content here? *)
      let verbose = None in
      !CallBack.cb.trace "feedback" ?verbose ("!!! feedback received in " ^ part)
end

module Report = struct
  let message_ ~io ~lvl ~message = io.CallBack.message ~lvl ~message
  let msg ~io ~lvl = Format.kasprintf (fun m -> message_ ~io ~lvl ~message:m)
  let diagnostics ~io ~uri ~version d = io.CallBack.diagnostics ~uri ~version d

  let fileProgress ~io ~uri ~version d =
    io.CallBack.fileProgress ~uri ~version d

  let perfData ~io ~uri ~version pd = io.CallBack.perfData ~uri ~version pd
  let serverVersion ~io vi = io.CallBack.serverVersion vi
  let serverStatus ~io st = io.CallBack.serverStatus st
end
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct