# `KinoIsabelle.Session`
[🔗](https://github.com/jcschuster/kino_isabelle/blob/v0.1.0-alpha.1/lib/kino_isabelle/session.ex#L1)

The runtime's Isabelle server and its logic sessions.

The server is started on the first check and each logic session (`"HOL"`, …)
on the first check that names it. Both live as long as this process: a
watchdog kills the server when this process or the whole VM exits. If the
connection dies, this process exits and its supervisor restarts it, so the
next check starts afresh.

The last result per theory file is cached and returned while the source and
logic session are unchanged.

# `child_spec`

Returns a specification to start this module under a supervisor.

See `Supervisor`.

# `start_link`

# `use_theories`

Writes and checks `theory` in the logic session `logic`.

Returns the raw `use_theories` result, or the failed task's result when
Isabelle rejects the theory header.

---

*Consult [api-reference.md](api-reference.md) for complete listing*