package coq-lsp

  1. Overview
  2. Docs
Language Server Protocol native server for Coq

Install

Dune Dependency

Authors

Maintainers

Sources

coq-lsp-0.2.3.8.19.tbz
sha256=dd5d0993261d3742e77ccac8344307d97b507b265d8743ae0ce33d0b3fcfd98a
sha512=76727400b27900fdd659af7f03c5f2cd979f50ea0c76ad6f5b5de56a53b9db06dba1e1c786fd3e8ab695e42d94c53d58415c0c5b5eef8192f9863eaf7dcca693

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

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
(************************************************************************)
(* 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 F = Format
module J = Yojson.Safe

(** {1 JSON-RPC input/output} *)

(* This needs a fix as to log protocol stuff not using the protocol *)
let log_protocol = ref (fun _ _ -> ())
let set_log_fn fn = log_protocol := fn

let read_raw_message ic =
  let cl = input_line ic in
  let sin = Scanf.Scanning.from_string cl in
  let raw_obj =
    Scanf.bscanf sin "Content-Length: %d\r" (fun size ->
        let buf = Bytes.create size in
        (* Consume the second \r\n or header *)
        let ohdr = input_line ic in
        (* If the second line is a return, then no more headers *)
        let () =
          if ohdr.[0] = '\r' then ()
          else
            (* Fixme (or use ocaml-lsp) Skip the Content-type header *)
            ignore (input_line ic)
        in
        really_input ic buf 0 size;
        Bytes.to_string buf)
  in
  J.from_string raw_obj

let read_raw_message ic =
  try Some (Ok (read_raw_message ic)) with
  (* if the end of input is encountered while some more characters are needed to
     read the current conversion specification, or the lsp server closes *)
  | End_of_file -> None
  (* if the input does not match the format. *)
  | Scanf.Scan_failure msg
  (* if a conversion to a number is not possible. *)
  | Failure msg
  (* if the format string is invalid. *)
  | Invalid_argument msg -> Some (Error msg)

let read_message ic =
  match read_raw_message ic with
  | None -> None (* EOF *)
  | Some (Ok com) ->
    !log_protocol "read" com;
    Some (Base.Message.of_yojson com)
  | Some (Error err) -> Some (Error err)

let mut = Mutex.create ()

let send_json fmt obj =
  Mutex.lock mut;
  !log_protocol "send" obj;
  let msg =
    if !Fleche.Config.v.pp_json then
      F.asprintf "%a" J.(pretty_print ~std:true) obj
    else J.to_string obj ^ "\n"
  in
  let size = String.length msg in
  F.fprintf fmt "Content-Length: %d\r\n\r\n%s%!" size msg;
  Mutex.unlock mut

let send_message fmt message = send_json fmt (Base.Message.to_yojson message)
OCaml

Innovation. Community. Security.