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

Livebook smart cell for Isabelle theories.

The "Isabelle theory" smart cell edits theory text and checks it with
`check/2` on the runtime's shared Isabelle server.

# `check`

```elixir
@spec check(String.t(), keyword()) ::
  {:ok, KinoIsabelle.Result.t()} | {:error, term()}
```

Checks `text` as an Isabelle theory.

Options:

  * `:session` - logic session, default `"HOL"`
  * `:theory` - theory name, default `"Scratch"`
  * `:imports` - imported theories, default `["Main"]`
  * `:header_mode` - `:auto` (default) wraps `text` in a theory header using
    `:theory` and `:imports`; `:manual` expects a complete theory

Returns `{:ok, result}` also when the theory has errors; `{:error, reason}`
when Isabelle could not be run.

---

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