Description
Supplies an optional sole-writer WebSocket lifecycle above the raw API.
Cancelled
function Cancelled (Item : Session) return Boolean
Report owner-side failure or disconnect cancellation.
Parameters
- Item
WebSocket session
Return value
True when Run requested producer cancellation
Close
procedure Close (Item : in out Session)
Request a normal server close after queued messages drain.
Parameters
- Item
WebSocket session
Close_Handler
type Close_Handler is access procedure
(X : in out Applications.Exchange; Item : in out Session);
Lifecycle callback invoked once after a peer or server close.
Parameters
- X
Borrowed request exchange
- Item
Request-scoped WebSocket session
Default_Session_Bytes
Default_Session_Bytes : constant := 256 * 1_024;
Default aggregate payload bytes retained by one session.
Max_Queued_Message_Bytes
Max_Queued_Message_Bytes : constant := 64 * 1_024;
Maximum payload bytes retained by one queued message.
Message_Handler
type Message_Handler is access procedure
(X : in out Applications.Exchange;
Item : in out Session;
Kind : WebSocket_Data_Kind;
Data : Flyology.Bytes.Unbounded_Bytes);
Lifecycle callback for one fully reassembled inbound message.
Parameters
- X
Borrowed request exchange
- Item
Request-scoped WebSocket session
- Kind
Text or binary message kind
- Data
Complete message payload
Open_Handler
type Open_Handler is access procedure
(X : in out Applications.Exchange; Item : in out Session);
Lifecycle callback invoked by the sole connection owner. It may inspect the Exchange and enqueue through Session, but must not retain either.
Parameters
- X
Borrowed request exchange
- Item
Request-scoped WebSocket session
Outgoing_Message
type Outgoing_Message is record
Kind : WebSocket_Data_Kind := Text_Frame;
Data : Flyology.Bytes.Unbounded_Bytes;
end record;
One queued outgoing WebSocket application message.
Record fields
- Kind
Text or binary frame
- Data
Complete message payload
Publish
procedure Publish
(Item : in out Session;
Value : Outgoing_Message;
Accepted : out Boolean)
Enqueue with backpressure, or return Accepted false after close. Owner-thread lifecycle callbacks should use Try_Publish to avoid waiting on their own queue.
Parameters
- Item
WebSocket session
- Value
Outgoing message
- Accepted
Whether the message was queued
Raised exceptions
- Program_Error
Item is configured for moved buffers
Publish_For
procedure Publish_For
(Item : in out Session;
Value : Outgoing_Message;
Accepted : out Boolean;
Timeout : Duration;
Timed_Out : out Boolean;
Token : access Flyology.Cancellation.Token := null)
Enqueue with bounded, cancellation-aware backpressure.
Parameters
- Item
WebSocket session
- Value
Outgoing message
- Accepted
Whether the message was queued
- Timeout
Maximum monotonic wait
- Timed_Out
Whether Timeout expired while the queue stayed full
- Token
Optional cancellation source
Raised exceptions
- Program_Error
Item is configured for moved buffers
Publish_Move
procedure Publish_Move
(Item : in out Session;
Kind : WebSocket_Data_Kind;
Value : in out Flyology.Buffers.Unique_Buffer;
Accepted : out Boolean)
Enqueue a pooled payload by transferring ownership without copying. Item must be configured with Value's pool. Success leaves Value vacant; close or admission failure preserves it.
Parameters
- Item
WebSocket session with a configured buffer pool
- Kind
Text or binary frame
- Value
Acquired payload buffer
- Accepted
Whether ownership transferred to the session
Publish_Move_For
procedure Publish_Move_For
(Item : in out Session;
Kind : WebSocket_Data_Kind;
Value : in out Flyology.Buffers.Unique_Buffer;
Accepted : out Boolean;
Timeout : Duration;
Timed_Out : out Boolean;
Token : access Flyology.Cancellation.Token := null)
Enqueue a pooled payload with bounded, cancellation-aware backpressure. Timeout or close preserves Value.
Parameters
- Item
WebSocket session with a configured buffer pool
- Kind
Text or binary frame
- Value
Acquired payload buffer
- Accepted
Whether ownership transferred to the session
- Timeout
Maximum monotonic wait
- Timed_Out
Whether Timeout expired before transfer
- Token
Optional cancellation source
Run
procedure Run
(X : in out Applications.Exchange;
Item : in out Session;
Open : access procedure
(X : in out Applications.Exchange; Item : in out Session) := null;
Message : access procedure
(X : in out Applications.Exchange;
Item : in out Session;
Kind : WebSocket_Data_Kind;
Data : Flyology.Bytes.Unbounded_Bytes) := null;
Closed : access procedure
(X : in out Applications.Exchange; Item : in out Session) := null;
Protocol : String := "";
Origin_Policy : WebSocket_Origin_Policy := Reject_Browser_Origins;
Allowed_Origin : String := "";
Max_Message : Natural := Default_Max_WebSocket_Message;
Receive_Quantum : Duration := 0.05;
Max_Outgoing_Burst : Positive := 16;
Metric_Output : access Metrics.Sink'Class := null;
Compression : WebSocket_Compression_Mode :=
No_WebSocket_Compression)
Upgrade, invoke lifecycle callbacks, serialize outgoing writes, and receive until either peer or application closes. A short receive quantum lets an idle peer coexist with mailbox producers without a second connection writer. The absolute Exchange deadline remains authoritative.
Parameters
- X
Request exchange
- Item
WebSocket session
- Open
Optional open callback
- Message
Optional inbound-message callback
- Closed
Optional close callback
- Protocol
Optional selected subprotocol
- Origin_Policy
Explicit browser-origin policy
- Allowed_Origin
Exact origin for Require_Exact_Origin
- Max_Message
Maximum retained/reassembled inbound message bytes
- Receive_Quantum
Maximum idle receive interval
- Max_Outgoing_Burst
Messages sent before servicing inbound frames
- Metric_Output
Optional lifecycle metric sink
- Compression
Explicit RFC 7692 negotiation policy
Session
type Session
(Capacity : Positive := 32;
Byte_Limit : Positive := Default_Session_Bytes;
Budget : access Outbound_Budget := null;
Buffer_Pool : access Flyology.Buffers.Pool := null) is limited private;
Request-scoped WebSocket session. Producer tasks may enqueue messages but cannot access the connection. Exactly one handler calls Run, and the session must not outlive that handler's Exchange scope.
Record fields
- Capacity
Maximum queued outgoing messages
- Byte_Limit
Maximum retained payload bytes in this session
- Budget
Optional shared server/application outbound budget
- Buffer_Pool
Optional pool enabling ownership-transfer publishing; the access discriminant requires the pool to outlive the session
Try_Publish
procedure Try_Publish
(Item : in out Session;
Value : Outgoing_Message;
Accepted : out Boolean)
Attempt to enqueue without waiting.
Parameters
- Item
WebSocket session
- Value
Outgoing message
- Accepted
Whether the message was queued
Raised exceptions
- Program_Error
Item is configured for moved buffers
Try_Publish_Move
procedure Try_Publish_Move
(Item : in out Session;
Kind : WebSocket_Data_Kind;
Value : in out Flyology.Buffers.Unique_Buffer;
Accepted : out Boolean)
Attempt to transfer a pooled payload without waiting.
Parameters
- Item
WebSocket session with a configured buffer pool
- Kind
Text or binary frame
- Value
Acquired payload buffer
- Accepted
Whether ownership transferred to the session