doc-src/System/Thy/document/Interfaces.tex

discontinued XSYMBOL_INSTALLFONTS (cf. 40fab092d2a2);

%
\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: