package coq-lsp
Language Server Protocol native server for Coq
Install
Dune Dependency
Authors
Maintainers
Sources
coq-lsp-0.1.9.8.19.tbz
sha256=ef664281ab6e242dd79374cbbe4f177f2f071d3457cd3b75c23643948d475961
sha512=3c180c0c2e1218936b6cacb37197370cf80be4c372c46e38a2ab403a5a6e99cd6403f927ecfc017aefa2ead856abb389d48feb183049bf2c7badb029ce13f1ee
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)"
>