package coq-lsp
Language Server Protocol native server for Coq
Install
Dune Dependency
Authors
Maintainers
Sources
coq-lsp-0.1.9.8.17.tbz
sha256=a89d86ed8b19d09bf3a06acbed690ae2859a7343d9faa03537c76cd492371651
sha512=edae491b284d5ab586c82cea4003a5b477f41ab25a4659431d4bc8caaee39b62de03b64d088ab8c528416210f88f73d4dfe5efbd32b22c70b75c9d18999c1e00
doc/src/petanque_json/interp.ml.html
Source file interp.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
open Protocol module A = Petanque.Agent let do_request ~token (module R : Request.S) ~id ~params = match R.Handler.Params.of_yojson (`Assoc params) with | Ok params -> ( match R.Handler.handler ~token params with | Ok result -> let result = R.Handler.Response.to_yojson result in Lsp.Base.Response.mk_ok ~id ~result | Error err -> let message = A.Error.to_string err in let code = A.Error.to_code err in Lsp.Base.Response.mk_error ~id ~code ~message) | Error message -> (* JSON-RPC Parse error *) let code = -32700 in Lsp.Base.Response.mk_error ~id ~code ~message let handle_request ~token ~id ~method_ ~params = match method_ with | s when String.equal Init.method_ s -> do_request ~token (module Init) ~id ~params | s when String.equal Start.method_ s -> do_request ~token (module Start) ~id ~params | s when String.equal RunTac.method_ s -> do_request ~token (module RunTac) ~id ~params | s when String.equal Goals.method_ s -> do_request ~token (module Goals) ~id ~params | s when String.equal Premises.method_ s -> do_request ~token (module Premises) ~id ~params | _ -> (* JSON-RPC method not found *) let code = -32601 in let message = "method not found" in Lsp.Base.Response.mk_error ~id ~code ~message let interp ~token (r : Lsp.Base.Message.t) : Yojson.Safe.t option = match r with | Request { id; method_; params } -> let response = handle_request ~token ~id ~method_ ~params in let response = Lsp.Base.Response.to_yojson response in Some response | Notification { method_ = _; params = _ } -> None | Response _ -> (* XXX: to implement *) None
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>