Keep an event stream connected.

Use one event-stream API on all three HTTP versions.

Flyology.HTTP.Client.SSE consumes the text/event-stream format. Server-sent events define an event-stream representation and reconnect processing model. They are not a separate HTTP wire protocol.

The existing client selects HTTP/1.1, HTTP/2, or HTTP/3. The SSE package uses the selected response-body stream without exposing protocol framing. Parsing, event dispatch, reconnect delay, last-event ID, deadline, and cancellation behavior remain the same across the three paths.

Choose and configure the protocol through the ordinary client API. The SSE call sites do not change when the configured protocol changes. To produce an event stream, use the response primitives or bounded mailbox lifecycle in the server guide.

Open bounded reconnect state without network I/O.

An Event_Source borrows an origin-bound client and retains parser and reconnect state. Its discriminant bounds the current input line, event fields, and event ID retained by the parser.

Call Open with a Request template, caller-selected delay limits, and one absolute deadline. Open resets local state but performs no network I/O. The first read starts the request.

with Flyology.HTTP.Client;
with Flyology.HTTP.Client.SSE;

package Client renames Flyology.HTTP.Client;
package SSE renames Flyology.HTTP.Client.SSE;

HTTP    : aliased Client.Client (Capacity => 2);
Request : Client.Request;
Source  : aliased SSE.Event_Source
  (HTTP'Access, Maximum_Event_Bytes => 64 * 1_024);

Client.Set_Target (Request, "/events");
SSE.Open
  (Source, Request,
   Initial_Reconnect_Delay => 1.0,
   Maximum_Reconnect_Delay => 60.0,
   Deadline                => Client.Deadline_After (300.0));

The source copies the target, headers, and redirect policy. It makes that copy a bodyless GET and controls the Accept: text/event-stream and Last-Event-ID fields. Configure same-origin redirects on the request template when the stream endpoint can redirect.

The Deadline_After call above produces one absolute deadline. That deadline covers the initial request, every response-body read, every reconnect wait, and every later request. A successful event does not restart it.

Read one dispatched event at a time.

The blocking Read procedure returns a Read_Result and, when available, one Event. It waits through connection establishment, partial body input, and any reconnects needed before the next event.

Event  : SSE.Event;
Result : SSE.Read_Result;

loop
   SSE.Read (Source, Result, Event);
   exit when Result = SSE.Stream_Stopped;

   Consume
     (SSE.Event_Type (Event),
      SSE.Data (Event),
      SSE.Last_Event_ID (Event));
end loop;

Data joins multiple data fields with LF. Event_Type returns message when the stream supplies no event field. The event overload of Last_Event_ID returns the ID current when that event was dispatched.

Input is decoded as UTF-8. Malformed sequences become U+FFFD. Lines without a recognized field and comment lines do not produce an event.

Let the source carry reconnect state.

Clean end of body and recoverable transport failure wait for the current reconnect delay, then start another request. An accepted decimal retry field replaces that delay in milliseconds.

An accepted id field becomes the next Last-Event-ID value when the dispatch boundary commits it. An empty id field clears the value.

The source overload of Last_Event_ID reports the value for the next reconnect. Reconnect_Delay reports the current delay.

Compose the same read with surrounding work.

The composable Read function constructs a Read_Operation in the caller’s completion set. Wait for that set alone, or combine the operation with timers, gates, cancellation, and other work described in the operations guide.

Set : aliased Flyology.Operations.Completion_Set (4);

declare
   Operation : SSE.Read_Operation :=
     SSE.Read (Set'Access, Source'Access, Token => null);
begin
   Flyology.Operations.Wait_All (Set);
   SSE.Finish (Operation, Result, Event);
end;

Call Finish after terminal completion to consume the typed result or raise the retained failure. The example uses the four-slot completion set maintained by the repository examples and protocol integration tests. Account separately for any surrounding operations placed in the same set.

For repeated reads, establish an operation once and start it again with the reusable Read procedure after the preceding result has been finished.

SSE.Read
  (Source'Access,
   Token     => Token'Access,
   Operation => Operation);

Flyology.Operations.Wait_All (Set);
SSE.Finish (Operation, Result, Event);

The blocking procedure waits over this composable implementation. It does not maintain a second parser or reconnect state machine.

Keep borrowed state alive through terminal drain.

• The client must outlive its event source.
• The event source must outlive an active composable read and remain alive through Finish or cancellation drain.
• A supplied cancellation token must also outlive that drain.
• The completion set must outlive the operation created in it.
• Only one read may be active on an event source. Do not call Open or start another read until the active operation is finished.

A concurrent read, or an attempt to reopen an active source, raises Program_Error. Use distinct event sources when the application needs concurrent streams.

Distinguish a permanent stop from a failed stream.

These fatal outcomes do not schedule another reconnect. A transport failure is reconnectable only when the client classifies the failed request or body read as recoverable.

Check protocol tests and reconnect assurance separately.

The behavioral suite exercises EventSource parsing, controlled request headers, fragmented input, reconnect delay, last-event ID updates, UTF-8 replacement, HTTP 204, the blocking overload, and the composable overload. Integration cases run the client through HTTP/1.1, HTTP/2, and HTTP/3 server paths.

The maintained SSE client assurance record maps the production reconnect policy to TLA+. TLC explores bounded lifecycle states. TLAPS proves the stated safety and termination lemmas. Generated traces replay through the Ada policy adapter.

Run ./scripts/check-sse-client-formal.sh for the formal gate and ./scripts/test.sh for the repository behavioral suite.