# HG changeset patch # User wenzelm # Date 1343473193 -7200 # Node ID af0f5560ac94f94fbe34f0b88290146aafbca3c3 # Parent d68b74435605248770dbbe0516e90dc2ff593692 misc tuning; diff -r d68b74435605 -r af0f5560ac94 doc-src/System/Thy/Interfaces.thy --- 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} *} diff -r d68b74435605 -r af0f5560ac94 doc-src/System/Thy/document/Interfaces.tex --- 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}% diff -r d68b74435605 -r af0f5560ac94 lib/Tools/tty --- 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 }