(* $Id$ *)

theory Interfaces

imports Pure

begin

chapter {* User interfaces *}

section {* Plain TTY interaction \label{sec:tool-tty} *}

text {*

  The @{tool_def tty} tool runs the Isabelle process interactively

  within a plain terminal session:

\begin{ttbox}

Usage: tty [OPTIONS]

  Options are:

    -l NAME      logic image name (default ISABELLE_LOGIC)

    -m MODE      add print mode for output

    -p NAME      line editor program name (default ISABELLE_LINE_EDITOR)

  Run Isabelle process with plain tty interaction, and optional line editor.

\end{ttbox}

  The @{verbatim "-l"} option specifies the logic image.  The

  @{verbatim "-m"} option specifies additional print modes.  The The

  @{verbatim "-p"} option specifies an alternative line editor (such

  as the @{executable_def rlwrap} wrapper for GNU readline); the

  fall-back is to use raw standard input.

  Regular interaction is via the standard Isabelle/Isar toplevel loop.

  The Isar command @{command exit} drops out into the raw ML system,

  which is occasionally useful for low-level debugging.  Invoking @{ML

  Isar.loop}~@{verbatim "();"} in ML will return to the Isar toplevel.

*}

section {* Proof General / Emacs *}

text {*

  The @{tool_def emacs} tool invokes a version of Emacs and Proof

  General within the regular Isabelle settings environment

  (\secref{sec:settings}).  This is more robust than starting Emacs

  separately, loading the Proof General lisp files, and then

  attempting to start Isabelle with dynamic @{setting PATH} lookup

  etc.

  The actual interface script is part of the Proof General

  distribution~\cite{proofgeneral}; its usage depends on the

  particular version.  There are some options available, such as

  @{verbatim "-l"} for passing the logic image to be used by default,

  or @{verbatim "-m"} to tune the standard print mode.  The following

  Isabelle settings are particularly important for Proof General:

  \begin{description}

  \item[@{setting_def PROOFGENERAL_HOME}] points to the main

  installation directory of the Proof General distribution.  The

  default settings try to locate this in a number of standard places,

  notably @{verbatim "$ISABELLE_HOME/contrib/ProofGeneral"}.

  \item[@{setting_def PROOFGENERAL_OPTIONS}] is implicitly prefixed to

  the command line of any invocation of the Proof General @{verbatim

  interface} script.

  \item[@{setting_def XSYMBOL_INSTALLFONTS}] may contain a small shell

  script to install the X11 fonts required for the X-Symbols mode of

  Proof General.  This is only relevant if the X11 display server runs

  on a different machine than the Emacs application, with a different

  file-system view on the Proof General installation.  Under most

  circumstances Proof General is able to refer to the font files that

  are part of its distribution.

  \end{description}

*}

end