package why3find

  1. Overview
  2. Docs
A Why3 Package Manager

Install 

dune-project
 Dependency

git.frama-c.com Readme Changelog LGPL-2.1-only License Edit opam file Versions (3)

Authors

  1. L
    Loïc Correnson <loic.correnson@cea.fr>
  2. B
    Benjamin Jorge <benjamin.jorge@cea.fr>

Maintainers

  1. B
    benjamin.jorge@cea.fr
  2. L
    loic.correnson@cea.fr

Sources

why3find-1.3.0.tar.gz
md5=435da830a513fd91ec5411c91126b763
sha512=fd8b04eb16d569c0dc9e5595a40b174d7858121b080c81d459b2f28fb3af1ebc32ef408859d5c1c5f45c61790625c027c2ecfc3d45e597943543de7212bab8d6

doc/why3find.utils/Why3findUtils/Lsp/index.html

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