doc-src/System/Thy/Interfaces.thy

removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
separate chapter on interfaces as Isabelle tools;

(* $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