Opaque handle for an open Isabelle server session.
Wraps a IsabelleClient.Shared GenServer PID — which owns the underlying
TCP socket, the active Isabelle session, and routes async task messages so
multiple concurrent callers can share it safely — together with the resolved
configuration the session was opened with, so follow-up calls can pick up
the same local_dir / isabelle_dir without being passed them again.
Construct only via AtpClient.Isabelle.open_session/1; tear down via
AtpClient.Isabelle.close_session/1. The struct's field names and
shapes are not part of the public contract — access via . from
outside this module is a dialyzer opacity violation, use
client/1, owner/1, config/1 instead.
Summary
Functions
Returns the underlying IsabelleClient.Shared GenServer pid — the one
that owns the TCP socket and routes async task messages.
Returns the resolved config the session was opened with — used by
follow-up prove_* calls so the caller doesn't have to re-supply
:local_dir, :isabelle_dir, and friends on every request.
Constructs a Session from its component pids and the resolved config.
Internal — called only from AtpClient.Isabelle.open_session/1.
Returns the pid of the private owner process that isolates the
Shared process's link from the caller. Used by close_session/1 and
by tests that need to monitor the session's teardown lifecycle.
Types
Functions
Returns the underlying IsabelleClient.Shared GenServer pid — the one
that owns the TCP socket and routes async task messages.
Returns the resolved config the session was opened with — used by
follow-up prove_* calls so the caller doesn't have to re-supply
:local_dir, :isabelle_dir, and friends on every request.
Constructs a Session from its component pids and the resolved config.
Internal — called only from AtpClient.Isabelle.open_session/1.
Returns the pid of the private owner process that isolates the
Shared process's link from the caller. Used by close_session/1 and
by tests that need to monitor the session's teardown lifecycle.