--- a/doc-src/System/Thy/Interfaces.thy Sat Jul 28 07:26:37 2012 +0200
+++ b/doc-src/System/Thy/Interfaces.thy Sat Jul 28 12:59:53 2012 +0200
@@ -10,14 +10,14 @@
The @{tool_def tty} tool runs the Isabelle process interactively
within a plain terminal session:
\begin{ttbox}
-Usage: tty [OPTIONS]
+Usage: isabelle 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.
+ Run Isabelle process with plain tty interaction and line editor.
\end{ttbox}
The @{verbatim "-l"} option specifies the logic image. The
@@ -27,39 +27,40 @@
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.
-*}
+ The Isar command @{command exit} drops out into the bare-bones ML
+ system, which is occasionally useful for debugging of the Isar
+ infrastructure itself. 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.
+text {* The @{tool_def emacs} tool invokes a version of Emacs and
+ Proof General \cite{proofgeneral} within the regular Isabelle
+ settings environment (\secref{sec:settings}). This is more
+ convenient 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:
+ distribution; 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"}.
+ installation directory of the Proof General distribution. This is
+ implicitly provided for versions of Proof General that are
+ distributed as Isabelle component, see also \secref{sec:components};
+ otherwise it needs to be configured manually.
\item[@{setting_def PROOFGENERAL_OPTIONS}] is implicitly prefixed to
the command line of any invocation of the Proof General @{verbatim
- interface} script.
+ interface} script. This allows to provide persistent default
+ options for the invocation of \texttt{isabelle emacs}.
\end{description}
*}
--- a/doc-src/System/Thy/document/Interfaces.tex Sat Jul 28 07:26:37 2012 +0200
+++ b/doc-src/System/Thy/document/Interfaces.tex Sat Jul 28 12:59:53 2012 +0200
@@ -30,14 +30,14 @@
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]
+Usage: isabelle 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.
+ Run Isabelle process with plain tty interaction and line editor.
\end{ttbox}
The \verb|-l| option specifies the logic image. The
@@ -47,8 +47,10 @@
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.%
+ The Isar command \hyperlink{command.exit}{\mbox{\isa{\isacommand{exit}}}} drops out into the bare-bones ML
+ system, which is occasionally useful for debugging of the Isar
+ infrastructure itself. Invoking \verb|Isar.loop|~\verb|();|
+ in ML will return to the Isar toplevel.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -57,29 +59,31 @@
\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 \indexdef{}{tool}{emacs}\hypertarget{tool.emacs}{\hyperlink{tool.emacs}{\mbox{\isa{\isatt{emacs}}}}} tool invokes a version of Emacs and
+ Proof General \cite{proofgeneral} within the regular Isabelle
+ settings environment (\secref{sec:settings}). This is more
+ convenient 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:
+ distribution; 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|.
+ installation directory of the Proof General distribution. This is
+ implicitly provided for versions of Proof General that are
+ distributed as Isabelle component, see also \secref{sec:components};
+ otherwise it needs to be configured manually.
\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.
+ the command line of any invocation of the Proof General \verb|interface| script. This allows to provide persistent default
+ options for the invocation of \texttt{isabelle emacs}.
\end{description}%
\end{isamarkuptext}%
--- a/lib/Tools/tty Sat Jul 28 07:26:37 2012 +0200
+++ b/lib/Tools/tty Sat Jul 28 12:59:53 2012 +0200
@@ -17,7 +17,7 @@
echo " -p NAME line editor program name"
echo " (default ISABELLE_LINE_EDITOR=\"$ISABELLE_LINE_EDITOR\")"
echo
- echo " Run Isabelle process with plain tty interaction, and optional line editor."
+ echo " Run Isabelle process with plain tty interaction and line editor."
echo
exit 1
}