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>
23 lines
805 B
Plaintext
23 lines
805 B
Plaintext
package openidea:plugin@1.6.0;
|
|
|
|
/// Optional export (world `plugin-diagnostics`): problems in the current,
|
|
/// possibly unsaved document, for the languages declared with the
|
|
/// `diagnostics` provider kind. Asked shortly after a document opens or
|
|
/// changes, under the editor-provider budget; it can't ask the user.
|
|
interface diagnostics-provider {
|
|
use diagnostics.{diagnostic};
|
|
|
|
/// The document to check (the editor's text, unsaved edits included).
|
|
record document {
|
|
/// Absolute path.
|
|
path: string,
|
|
language: string,
|
|
version: u64,
|
|
text: string,
|
|
}
|
|
|
|
/// The document's problems, at most 5,000; they replace what this
|
|
/// provider reported before, and an empty list removes them.
|
|
diagnostics: func(doc: document) -> list<diagnostic>;
|
|
}
|