package coq-lsp

  1. Overview
  2. Docs
Language Server Protocol native server for Coq

Install

dune-project
 Dependency

Authors

Maintainers

Sources

coq-lsp-0.1.9.8.18.tbz
sha256=99514bcbf82318b9ff857656f4ec1f87bb46f1c699a4f1e9fb06f5fcdd8d8839
sha512=fa4593a2ae416e554869a879da5d35a1d33efa5cc8743f77c05373875ecea267019989dec600d5e880d909aea97ce7f6990ac59e58aabce358e3693b0764bef8

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
OCaml

Innovation. Community. Security.