Module Why3findUtils.LspSource

LSP Server Protocol

Sourcetype server
Sourcetype response = (Json.t, Json.t) result
Sourceval establish : Rpc.transport -> server

Establish the server or exit

Sourceval shutdown : server -> unit

Shutdown the server

Sourceval running : server -> bool

Testing if the server is still running. Returns true when there is no more in/out pending messages.

Sourceval yield : server -> unit

Only process pending I/O (non-blocking).

Sourceval process : server -> bool

Process (at most) one pending LSP message, if any (non-blocking). First, yield the server to process pending I/O. Then, process one LSP message, if any. Returns true is some request has been processed or not. This function immediately returns false when it is called during a request handler.

LSP Server Capabilities

Sourcetype capability
Sourceval register_capability : server -> string -> Json.t -> capability

Dynamically register a server capability. Can be unregistered mater with the returned capability.

Sourceval unregister_capability : server -> capability -> unit

Unregister a server capability.

LSP Request Handlers

Sourceval register : ?force:bool -> string -> (server -> Json.t -> Json.t) -> unit

Register a request or notification handler. Some builtin request and notifications are already registered and shall be forced updated, namely initialize, initialized, shutdown, exit and $/setTrace.

The callbacks may raise exceptions, in which case an error is reported to the client. Meaningfull exceptions are:

  • Not_found request is not supported
  • Invalid_argument _ request arguments are incorrect
  • Failure _ and any other exception are treated as internal error
Sourceval ignore : string -> unit

Ignore a request or notification.

Sourceval notify : server -> string -> Json.t -> unit

Notify the server

Sourceval send : server -> string -> ?callback:(response -> unit) -> Json.t -> unit

Send a request or notification to the server