package vscoq-language-server
VSCoq language server
Install
Dune Dependency
Authors
Maintainers
Sources
vscoq-language-server-2.2.6.tar.gz
md5=f528c1760966ac10d48b5f1c5531411a
sha512=1f69538ae5f78854b34e3f1a9d408714843e899bb96d063c2bfac410339b6a13ee5f30d5e7b3cd2bbd673169bcfdb550153ba741092cdc3ee3a8ca6446cc2240
doc/src/vscoq-language-server.dm/types.ml.html
Source file types.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(**************************************************************************) (* *) (* 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 Protocol.LspWrapper type sentence_id = Stateid.t type sentence_id_set = Stateid.Set.t module RangeList = struct type t = Range.t list let insert_or_merge_range r ranges = let ranges = List.sort Range.compare (r :: ranges) in let rec insert_or_merge_sorted_ranges r1 = function | [] -> [r1] | r2 :: l -> if Range.included ~in_:r1 r2 then (*since the ranges are sorted, only r2 can be included in r1*) insert_or_merge_sorted_ranges r1 l else if Range.prefixes ~in_:r2 r1 then begin let range = Range.{start = r1.Range.start; end_ = r2.Range.end_} in insert_or_merge_sorted_ranges range l end else r1 :: (insert_or_merge_sorted_ranges r2 l) in insert_or_merge_sorted_ranges (List.hd ranges) (List.tl ranges) let rec remove_or_truncate_range r = function | [] -> [] | r1 :: l -> if Range.equals r r1 then l else if Range.strictly_included ~in_: r1 r then Range.{ start = r1.Range.start; end_ = r.Range.start} :: Range.{ start = r.Range.end_; end_ = r1.Range.end_} :: l else if Range.prefixes ~in_:r1 r then Range.{ start = r.Range.end_; end_ = r1.Range.end_} :: l else if Range.postfixes ~in_:r1 r then Range.{ start = r1.Range.start; end_ = r.Range.start} :: l else r1 :: (remove_or_truncate_range r l) let rec cut_from_range r = function | [] -> [] | r1 :: l -> let (<=) x y = Position.compare x y <= 0 in if r.Range.start <= r1.Range.start then l else if r.Range.start <= r1.Range.end_ then Range.{start = r1.Range.start; end_ = r.Range.start} :: l else r1 :: (cut_from_range r l) end type exec_overview = { prepared: RangeList.t; processing : RangeList.t; processed : RangeList.t; } let empty_overview = {processing = []; processed = []; prepared = []} [%%if coq = "8.18" || coq = "8.19" || coq = "8.20"] module Quickfix = struct type t = unit let from_exception _ = Ok([]) let pp = Pp.mt let loc _ = Loc.make_loc (0,0) end [%%endif] type text_edit = Range.t * string type link = { write_to : Unix.file_descr; read_from: Unix.file_descr; } type error = { code: Jsonrpc.Response.Error.Code.t option; message: string; } type 'a log = Log : 'a -> 'a log