package coq-lsp
Language Server Protocol native server for Coq
Install
Dune Dependency
Authors
Maintainers
Sources
coq-lsp-0.1.3.v8.16.tbz
sha256=d6d589ae18453d9251b4250df50e59cfc87254de0e4734e13c5bca06ab14cee5
sha512=802b4673c7f581976526a3cb4bd824f7574c5b1cc8fcc7759fcd3358cdc3e4cebef3ec908899ad68129190777ccda931dfc1643b45db156ede15acae0382c148
doc/src/coq-lsp.coq/protect.ml.html
Source file protect.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
module Error = struct type payload = Loc.t option * Pp.t type t = | User of payload | Anomaly of payload let map ~f = function | User e -> User (f e) | Anomaly e -> Anomaly (f e) end module R = struct type 'a t = | Completed of ('a, Error.t) result | Interrupted (* signal sent, eval didn't complete *) let map ~f = function | Completed (Result.Ok r) -> Completed (Result.Ok (f r)) | Completed (Result.Error r) -> Completed (Result.Error r) | Interrupted -> Interrupted let map_error ~f = function | Completed (Error e) -> Completed (Error (Error.map ~f e)) | res -> res let map_loc ~f = let f (loc, msg) = (Option.map f loc, msg) in map_error ~f end (* Eval and reify exceptions *) let eval_exn ~f x = try let res = f x in R.Completed (Ok res) with | Sys.Break -> R.Interrupted | exn -> let e, info = Exninfo.capture exn in let loc = Loc.(get_loc info) in let msg = CErrors.iprint (e, info) in if CErrors.is_anomaly e then R.Completed (Error (Anomaly (loc, msg))) else R.Completed (Error (User (loc, msg))) module E = struct type 'a t = { r : 'a R.t ; feedback : Message.t list } let map ~f { r; feedback } = { r = R.map ~f r; feedback } let map_message ~f (loc, lvl, msg) = (Option.map f loc, lvl, msg) let map_loc ~f { r; feedback } = { r = R.map_loc ~f r; feedback = List.map (map_message ~f) feedback } end let fb_queue : Message.t list ref = ref [] (* Eval with reified exceptions and feedback *) let eval ~f x = let r = eval_exn ~f x in let feedback = List.rev !fb_queue in let () = fb_queue := [] in { E.r; feedback }
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>