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.fleche/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 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
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>