mirror of
https://github.com/l0ng-ai/openidea.git
synced 2026-11-14 16:07:52 +00:00
Lucas
43b5c69ecd
Plugins get a host-owned WebSocket resource (net.websocket-connect → websocket with id/send/drain/close; dropping it closes the transport). The connection is bound to the project it was opened for, needs the endpoint's net:<host> grant, uses WSS outside loopback with the shared rustls config, and is capped at eight per plugin. Request headers (secret placeholders expanded) go with the handshake, except the ones the handshake owns; an empty subprotocol requests none; the handshake is bounded by the call's I/O budget. Incoming frames queue in a bounded FIFO, signalled by the websocket-ready event. Checked-in components are rebuilt for API 1.6. Co-authored-by: SorPuti <56741582+SorPuti@users.noreply.github.com>
30 lines
948 B
Plaintext
30 lines
948 B
Plaintext
package openidea:plugin@1.6.0;
|
|
|
|
/// Optional export (world `plugin-hover`): Markdown added to the hover of
|
|
/// documents of the languages declared with the `hover` provider kind,
|
|
/// including languages the plugin doesn't contribute. It shows below the
|
|
/// language server's hover, under the edit-path budget.
|
|
interface hover-provider {
|
|
use types.{position, range};
|
|
|
|
/// The document hovered (the editor's text while it is open).
|
|
record document {
|
|
/// Absolute path.
|
|
path: string,
|
|
language: string,
|
|
version: u64,
|
|
text: string,
|
|
}
|
|
|
|
/// What the plugin adds to the hover.
|
|
record hover-content {
|
|
/// At most 64 KiB.
|
|
markdown: string,
|
|
/// The text the hover describes; used when the server names none.
|
|
range: option<range>,
|
|
}
|
|
|
|
/// The hover at `at`, or `none` to add nothing.
|
|
hover: func(doc: document, at: position) -> option<hover-content>;
|
|
}
|