package vscoq-language-server
VSCoq language server
Install
Dune Dependency
Authors
Maintainers
Sources
vscoq-language-server-2.1.3.tar.gz
md5=300d171d3225fac2a68ce348154ff640
sha512=65bc228d84f814cfea4b5ddcd20f365a8a8ea178bbd4474129c998e8a351a7dba8d2adbb263f7f18ed41c45c765e73c332b518834360bf3638fe2721518e1fd8
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 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
(**************************************************************************) (* *) (* 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 compare r1 r2 = match Position.compare r1.start r2.start with | 0 -> Position.compare r1.end_ r2.end_ | x -> x let equals r1 r2 = Position.compare r1.start r2.start == 0 && Position.compare r1.end_ r2.end_ == 0 let included ~in_ { start; end_ } = let (<=) x y = Position.compare x y <= 0 in in_.start <= start && end_ <= in_.end_ let strictly_included ~in_ { start; end_ } = let (<) x y = Position.compare x y < 0 in in_.start < start && end_ < in_.end_ let prefixes ~in_ { start; end_ } = let (<) x y = Position.compare x y < 0 in let (<=) x y = Position.compare x y <= 0 in start <= in_.start && end_ < in_.end_ && in_.start <= end_ let postfixes ~in_ { start; end_ } = let (<) x y = Position.compare x y < 0 in let (<=) x y = Position.compare x y <= 0 in start <= in_.end_ && in_.start < start && in_.end_ < end_ let to_string range = Format.sprintf ("Range (start: %s, end: %s)") (Position.to_string range.start) (Position.to_string range.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 overview = { uri : DocumentUri.t; preparedRange: Range.t list; processingRange : Range.t list; processedRange : Range.t list; } [@@deriving yojson] type notification = | QueryResultNotification of query_result
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>