# HG changeset patch # User wenzelm # Date 1228050226 -3600 # Node ID 0a802cdda3407b85a4d66759ed09fddba953c05a # Parent 0642cbb60c9827a8cd566929607639c734324cbd removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting; separate chapter on interfaces as Isabelle tools; diff -r 0642cbb60c98 -r 0a802cdda340 doc-src/System/IsaMakefile --- a/doc-src/System/IsaMakefile Sun Nov 30 14:03:45 2008 +0100 +++ b/doc-src/System/IsaMakefile Sun Nov 30 14:03:46 2008 +0100 @@ -22,7 +22,7 @@ Pure-System: $(LOG)/Pure-System.gz $(LOG)/Pure-System.gz: Thy/ROOT.ML ../antiquote_setup.ML \ - Thy/Basics.thy Thy/Misc.thy Thy/Presentation.thy + Thy/Basics.thy Thy/Misc.thy Thy/Interfaces.thy Thy/Presentation.thy @$(USEDIR) -s System Pure Thy diff -r 0642cbb60c98 -r 0a802cdda340 doc-src/System/Thy/Basics.thy --- a/doc-src/System/Thy/Basics.thy Sun Nov 30 14:03:45 2008 +0100 +++ b/doc-src/System/Thy/Basics.thy Sun Nov 30 14:03:46 2008 +0100 @@ -8,19 +8,18 @@ text {* This manual describes Isabelle together with related tools and user - interfaces as seen from an outside (system oriented) view. See also - the \emph{Isabelle/Isar Reference Manual}~\cite{isabelle-isar-ref} - and the \emph{Isabelle Reference Manual}~\cite{isabelle-ref} for the - actual Isabelle commands and related functions. + interfaces as seen from a system oriented view. See also the + \emph{Isabelle/Isar Reference Manual}~\cite{isabelle-isar-ref} for + the actual Isabelle input language and related concepts. - \medskip The Isabelle system environment emerges from a few general - concepts. + \medskip The Isabelle system environment provides the following + basic infrastructure to integrate tools smoothly. \begin{enumerate} - \item The \emph{Isabelle settings} mechanism provides environment - variables to all Isabelle programs (including tools and user - interfaces). + \item The \emph{Isabelle settings} mechanism provides process + environment variables to all Isabelle executables (including tools + and user interfaces). \item The \emph{raw Isabelle process} (@{executable_ref "isabelle-process"}) runs logic sessions either interactively or in @@ -33,11 +32,6 @@ user interfaces etc. Such tools automatically benefit from the settings mechanism. - \item The \emph{Isabelle interface wrapper} (@{executable_ref - "isabelle-interface"}) provides some abstraction over the actual - user interface to be used. The de-facto standard interface for - Isabelle is Proof~General \cite{proofgeneral}. - \end{enumerate} *} @@ -256,11 +250,6 @@ derives an individual directory for temporary files. The default is somewhere in @{verbatim "/tmp"}. - \item[@{setting_def ISABELLE_INTERFACE}] is an identifier that - specifies the actual user interface that the capital @{executable - Isabelle} or @{executable "isabelle-interface"} should invoke. See - \secref{sec:interface} for more details. - \end{description} *} @@ -480,41 +469,4 @@ by @{verbatim "isabelle make"} alone. *} - -section {* The Isabelle interface wrapper \label{sec:interface} *} - -text {* - Isabelle is a generic theorem prover, even w.r.t.\ its user - interface. The @{executable_def Isabelle} (or @{executable_def - "isabelle-interface"}) executable provides a uniform way for - end-users to invoke a certain interface; which one to start is - determined by the @{setting_ref ISABELLE_INTERFACE} setting - variable, which should give a full path specification to the actual - executable. - - Presently, the most prominent Isabelle interface is Proof - General~\cite{proofgeneral}\index{user interface!Proof General}. - The Proof General distribution includes an interface wrapper script - for the regular Isar toplevel, see @{verbatim - "ProofGeneral/isar/interface"}. The canonical settings for - Isabelle/Isar are as follows: - -\begin{ttbox} -ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface -PROOFGENERAL_OPTIONS="" -\end{ttbox} - - Thus @{executable Isabelle} would automatically invoke Emacs with - proper setup of the Proof General Lisp packages. 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. - - \medskip Note that the world may be also seen the other way round: - Emacs may be started first (with proper setup of Proof General - mode), and @{executable "isabelle-process"} run from within. This - requires further Emacs Lisp configuration, see the Proof General - documentation \cite{proofgeneral} for more information. -*} - end \ No newline at end of file diff -r 0642cbb60c98 -r 0a802cdda340 doc-src/System/Thy/Interfaces.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/System/Thy/Interfaces.thy Sun Nov 30 14:03:46 2008 +0100 @@ -0,0 +1,77 @@ +(* $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 \ No newline at end of file diff -r 0642cbb60c98 -r 0a802cdda340 doc-src/System/Thy/Misc.thy --- a/doc-src/System/Thy/Misc.thy Sun Nov 30 14:03:45 2008 +0100 +++ b/doc-src/System/Thy/Misc.thy Sun Nov 30 14:03:46 2008 +0100 @@ -12,46 +12,6 @@ *} -section {* The Proof General / Emacs interface *} - -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} -*} - - section {* Displaying documents *} text {* @@ -294,30 +254,6 @@ *} -section {* Run Isabelle with plain tty interaction \label{sec:tool-tty} *} - -text {* - The @{tool_def tty} utility 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. -*} - - section {* Remove awkward symbol names from theory sources *} text {* diff -r 0642cbb60c98 -r 0a802cdda340 doc-src/System/Thy/ROOT.ML --- a/doc-src/System/Thy/ROOT.ML Sun Nov 30 14:03:45 2008 +0100 +++ b/doc-src/System/Thy/ROOT.ML Sun Nov 30 14:03:46 2008 +0100 @@ -5,5 +5,6 @@ use "../../antiquote_setup.ML"; use_thy "Basics"; +use_thy "Interfaces"; use_thy "Presentation"; use_thy "Misc"; diff -r 0642cbb60c98 -r 0a802cdda340 doc-src/System/Thy/document/Basics.tex --- a/doc-src/System/Thy/document/Basics.tex Sun Nov 30 14:03:45 2008 +0100 +++ b/doc-src/System/Thy/document/Basics.tex Sun Nov 30 14:03:46 2008 +0100 @@ -26,19 +26,18 @@ % \begin{isamarkuptext}% This manual describes Isabelle together with related tools and user - interfaces as seen from an outside (system oriented) view. See also - the \emph{Isabelle/Isar Reference Manual}~\cite{isabelle-isar-ref} - and the \emph{Isabelle Reference Manual}~\cite{isabelle-ref} for the - actual Isabelle commands and related functions. + interfaces as seen from a system oriented view. See also the + \emph{Isabelle/Isar Reference Manual}~\cite{isabelle-isar-ref} for + the actual Isabelle input language and related concepts. - \medskip The Isabelle system environment emerges from a few general - concepts. + \medskip The Isabelle system environment provides the following + basic infrastructure to integrate tools smoothly. \begin{enumerate} - \item The \emph{Isabelle settings} mechanism provides environment - variables to all Isabelle programs (including tools and user - interfaces). + \item The \emph{Isabelle settings} mechanism provides process + environment variables to all Isabelle executables (including tools + and user interfaces). \item The \emph{raw Isabelle process} (\indexref{}{executable}{isabelle-process}\hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}}) runs logic sessions either interactively or in batch mode. In particular, this view abstracts over the invocation @@ -50,10 +49,6 @@ user interfaces etc. Such tools automatically benefit from the settings mechanism. - \item The \emph{Isabelle interface wrapper} (\indexref{}{executable}{isabelle-interface}\hyperlink{executable.isabelle-interface}{\mbox{\isa{\isatt{isabelle{\isacharminus}interface}}}}) provides some abstraction over the actual - user interface to be used. The de-facto standard interface for - Isabelle is Proof~General \cite{proofgeneral}. - \end{enumerate}% \end{isamarkuptext}% \isamarkuptrue% @@ -262,10 +257,6 @@ derives an individual directory for temporary files. The default is somewhere in \verb|/tmp|. - \item[\indexdef{}{setting}{ISABELLE\_INTERFACE}\hypertarget{setting.ISABELLE-INTERFACE}{\hyperlink{setting.ISABELLE-INTERFACE}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}INTERFACE}}}}}] is an identifier that - specifies the actual user interface that the capital \hyperlink{executable.Isabelle}{\mbox{\isa{\isatt{Isabelle}}}} or \hyperlink{executable.isabelle-interface}{\mbox{\isa{\isatt{isabelle{\isacharminus}interface}}}} should invoke. See - \secref{sec:interface} for more details. - \end{description}% \end{isamarkuptext}% \isamarkuptrue% @@ -492,43 +483,6 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isamarkupsection{The Isabelle interface wrapper \label{sec:interface}% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -Isabelle is a generic theorem prover, even w.r.t.\ its user - interface. The \indexdef{}{executable}{Isabelle}\hypertarget{executable.Isabelle}{\hyperlink{executable.Isabelle}{\mbox{\isa{\isatt{Isabelle}}}}} (or \indexdef{}{executable}{isabelle-interface}\hypertarget{executable.isabelle-interface}{\hyperlink{executable.isabelle-interface}{\mbox{\isa{\isatt{isabelle{\isacharminus}interface}}}}}) executable provides a uniform way for - end-users to invoke a certain interface; which one to start is - determined by the \indexref{}{setting}{ISABELLE\_INTERFACE}\hyperlink{setting.ISABELLE-INTERFACE}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}INTERFACE}}}} setting - variable, which should give a full path specification to the actual - executable. - - Presently, the most prominent Isabelle interface is Proof - General~\cite{proofgeneral}\index{user interface!Proof General}. - The Proof General distribution includes an interface wrapper script - for the regular Isar toplevel, see \verb|ProofGeneral/isar/interface|. The canonical settings for - Isabelle/Isar are as follows: - -\begin{ttbox} -ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface -PROOFGENERAL_OPTIONS="" -\end{ttbox} - - Thus \hyperlink{executable.Isabelle}{\mbox{\isa{\isatt{Isabelle}}}} would automatically invoke Emacs with - proper setup of the Proof General Lisp packages. 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. - - \medskip Note that the world may be also seen the other way round: - Emacs may be started first (with proper setup of Proof General - mode), and \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}} run from within. This - requires further Emacs Lisp configuration, see the Proof General - documentation \cite{proofgeneral} for more information.% -\end{isamarkuptext}% -\isamarkuptrue% -% \isadelimtheory % \endisadelimtheory diff -r 0642cbb60c98 -r 0a802cdda340 doc-src/System/Thy/document/Interfaces.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/System/Thy/document/Interfaces.tex Sun Nov 30 14:03:46 2008 +0100 @@ -0,0 +1,115 @@ +% +\begin{isabellebody}% +\def\isabellecontext{Interfaces}% +% +\isadelimtheory +\isanewline +\isanewline +% +\endisadelimtheory +% +\isatagtheory +\isacommand{theory}\isamarkupfalse% +\ Interfaces\isanewline +\isakeyword{imports}\ Pure\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 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{\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{\isacharunderscore}OPTIONS}}}}}] is implicitly prefixed to + the command line of any invocation of the Proof General \verb|interface| script. + + \item[\indexdef{}{setting}{XSYMBOL\_INSTALLFONTS}\hypertarget{setting.XSYMBOL-INSTALLFONTS}{\hyperlink{setting.XSYMBOL-INSTALLFONTS}{\mbox{\isa{\isatt{XSYMBOL{\isacharunderscore}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{isamarkuptext}% +\isamarkuptrue% +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +\isacommand{end}\isamarkupfalse% +% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +\end{isabellebody}% +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "root" +%%% End: diff -r 0642cbb60c98 -r 0a802cdda340 doc-src/System/Thy/document/Misc.tex --- a/doc-src/System/Thy/document/Misc.tex Sun Nov 30 14:03:45 2008 +0100 +++ b/doc-src/System/Thy/document/Misc.tex Sun Nov 30 14:03:46 2008 +0100 @@ -30,47 +30,6 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isamarkupsection{The Proof General / Emacs interface% -} -\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{\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{\isacharunderscore}OPTIONS}}}}}] is implicitly prefixed to - the command line of any invocation of the Proof General \verb|interface| script. - - \item[\indexdef{}{setting}{XSYMBOL\_INSTALLFONTS}\hypertarget{setting.XSYMBOL-INSTALLFONTS}{\hyperlink{setting.XSYMBOL-INSTALLFONTS}{\mbox{\isa{\isatt{XSYMBOL{\isacharunderscore}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{isamarkuptext}% -\isamarkuptrue% -% \isamarkupsection{Displaying documents% } \isamarkuptrue% @@ -329,32 +288,6 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isamarkupsection{Run Isabelle with plain tty interaction \label{sec:tool-tty}% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -The \indexdef{}{tool}{tty}\hypertarget{tool.tty}{\hyperlink{tool.tty}{\mbox{\isa{\isatt{tty}}}}} utility 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 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.% -\end{isamarkuptext}% -\isamarkuptrue% -% \isamarkupsection{Remove awkward symbol names from theory sources% } \isamarkuptrue% diff -r 0642cbb60c98 -r 0a802cdda340 doc-src/System/system.tex --- a/doc-src/System/system.tex Sun Nov 30 14:03:45 2008 +0100 +++ b/doc-src/System/system.tex Sun Nov 30 14:03:46 2008 +0100 @@ -20,7 +20,7 @@ \title{\includegraphics[scale=0.5]{isabelle} \\[4ex] The Isabelle System Manual} \author{\emph{Makarius Wenzel} and \emph{Stefan Berghofer} \\ - TU München} + TU M\"unchen} \makeindex @@ -31,6 +31,7 @@ \pagenumbering{roman} \tableofcontents \clearfirst \input{Thy/document/Basics.tex} +\input{Thy/document/Interfaces.tex} \input{Thy/document/Presentation.tex} \input{Thy/document/Misc.tex}