package coq-lsp
Language Server Protocol native server for Coq
Install
Dune Dependency
Authors
Maintainers
Sources
coq-lsp-0.1.4.v8.16.tbz
sha256=50df59eafc5b24a881c1a1dda6f6032b1da35b9b6ade7cb9e39968def9319508
sha512=e1d383b6802758cdbe5cbc6278af275d7951acd78224cdcfe622428942e84366ca283bf375d6e535ad7e8d8e847df84bd763bb2a263fc457dc5aead386c2836d
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 67
module Error = struct type 'l payload = 'l option * Pp.t type 'l t = | User of 'l payload | Anomaly of 'l payload let map ~f = function | User e -> User (f e) | Anomaly e -> Anomaly (f e) end module R = struct type ('a, 'l) t = | Completed of ('a, 'l 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)) | Completed (Ok r) -> Completed (Ok r) | Interrupted -> Interrupted 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, 'l) t = { r : ('a, 'l) R.t ; feedback : 'l 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 : Loc.t 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)"
>