package coq-lsp
Language Server Protocol native server for Coq
Install
Dune Dependency
Authors
Maintainers
Sources
coq-lsp-0.2.3.9.0.tbz
sha256=8776582dddfe768623870cf540ff6ba1e96a44a36e85db18ab93d238d640f92a
sha512=2837889bf99bfe715bd0e752782211a76a14aac71ed37a4fb784f4f0abe338352c9c6d8caa37daf79c036997add1cb306c523f793625b38709f3b5e245380223
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)
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>