%
\begin{isabellebody}%
\def\isabellecontext{Interfaces}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ Interfaces\isanewline
\isakeyword{imports}\ Base\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isamarkupchapter{User interfaces%
}
\isamarkuptrue%
%
\isamarkupsection{Plain TTY interaction \label{sec:tool-tty}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The \indexdef{}{tool}{tty}\hypertarget{tool.tty}{\hyperlink{tool.tty}{\mbox{\isa{\isatt{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 \verb|-l| option specifies the logic image. The
\verb|-m| option specifies additional print modes. The
\verb|-p| option specifies an alternative line editor (such
as the \indexdef{}{executable}{rlwrap}\hypertarget{executable.rlwrap}{\hyperlink{executable.rlwrap}{\mbox{\isa{\isatt{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 \hyperlink{command.exit}{\mbox{\isa{\isacommand{exit}}}} drops out into the raw ML system,
which is occasionally useful for low-level debugging. Invoking \verb|Isar.loop|~\verb|();| in ML will return to the Isar toplevel.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Proof General / Emacs%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The \indexdef{}{tool}{emacs}\hypertarget{tool.emacs}{\hyperlink{tool.emacs}{\mbox{\isa{\isatt{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 \hyperlink{setting.PATH}{\mbox{\isa{\isatt{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
\verb|-l| for passing the logic image to be used by default,
or \verb|-m| to tune the standard print mode. The following
Isabelle settings are particularly important for Proof General:
\begin{description}
\item[\indexdef{}{setting}{PROOFGENERAL\_HOME}\hypertarget{setting.PROOFGENERAL-HOME}{\hyperlink{setting.PROOFGENERAL-HOME}{\mbox{\isa{\isatt{PROOFGENERAL{\isaliteral{5F}{\isacharunderscore}}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 \verb|$ISABELLE_HOME/contrib/ProofGeneral|.
\item[\indexdef{}{setting}{PROOFGENERAL\_OPTIONS}\hypertarget{setting.PROOFGENERAL-OPTIONS}{\hyperlink{setting.PROOFGENERAL-OPTIONS}{\mbox{\isa{\isatt{PROOFGENERAL{\isaliteral{5F}{\isacharunderscore}}OPTIONS}}}}}] is implicitly prefixed to
the command line of any invocation of the Proof General \verb|interface| script.
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Isabelle/jEdit Prover IDE \label{sec:tool-jedit}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The \indexdef{}{tool}{jedit}\hypertarget{tool.jedit}{\hyperlink{tool.jedit}{\mbox{\isa{\isatt{jedit}}}}} tool invokes a version of jEdit that has
been augmented with some components to provide a fully-featured
Prover IDE (based on Isabelle/Scala):
\begin{ttbox}
Usage: isabelle jedit [OPTIONS] [FILES ...]
Options are:
-J OPTION add JVM runtime option (default JEDIT_JAVA_OPTIONS)
-b build only
-d enable debugger
-f fresh build
-j OPTION add jEdit runtime option (default JEDIT_OPTIONS)
-l NAME logic image name (default ISABELLE_LOGIC)
-m MODE add print mode for output
Start jEdit with Isabelle plugin setup and opens theory FILES
(default Scratch.thy).
\end{ttbox}
The \verb|-l| option specifies the logic image. The
\verb|-m| option specifies additional print modes.
The \verb|-J| and \verb|-j| options allow to pass
additional low-level options to the JVM or jEdit, respectively. The
defaults are provided by the Isabelle settings environment.
The \verb|-d| option allows to connect to the runtime debugger
of the JVM. Note that the Scala Console of Isabelle/jEdit is more
convenient in most practical situations.
The \verb|-b| and \verb|-f| options control the
self-build mechanism of Isabelle/jEdit. This is only relevant for
building from sources, which also requires an auxiliary \verb|jedit_build| component. Official Isabelle releases already include a
version of Isabelle/jEdit that is built properly.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: