TPTP editor Smart Cell with a backend mode switch.
The cell drives all four AtpClient backends — SystemOnTPTP, StarExec,
Isabelle, LocalExec — from a single TPTP problem editor. Switching the
backend dropdown swaps both the per-call controls in the header (solver
picker for SoTPTP, proof method for Isabelle, …) and the output rendering
(raw prover text for SoTPTP, normalized SZS badge for StarExec/LocalExec,
per-lemma table for Isabelle).
Cross-cutting credentials (StarExec base URL, Isabelle password, …) live in
KinoAtpClient.BackendConfig so this cell stays focused on a single
problem run.