1.1 --- a/doc-src/System/IsaMakefile Sun Nov 30 14:03:45 2008 +0100
1.2 +++ b/doc-src/System/IsaMakefile Sun Nov 30 14:03:46 2008 +0100
1.3 @@ -22,7 +22,7 @@
1.4 Pure-System: $(LOG)/Pure-System.gz
1.5
1.6 $(LOG)/Pure-System.gz: Thy/ROOT.ML ../antiquote_setup.ML \
1.7 - Thy/Basics.thy Thy/Misc.thy Thy/Presentation.thy
1.8 + Thy/Basics.thy Thy/Misc.thy Thy/Interfaces.thy Thy/Presentation.thy
1.9 @$(USEDIR) -s System Pure Thy
1.10
1.11
2.1 --- a/doc-src/System/Thy/Basics.thy Sun Nov 30 14:03:45 2008 +0100
2.2 +++ b/doc-src/System/Thy/Basics.thy Sun Nov 30 14:03:46 2008 +0100
2.3 @@ -8,19 +8,18 @@
2.4
2.5 text {*
2.6 This manual describes Isabelle together with related tools and user
2.7 - interfaces as seen from an outside (system oriented) view. See also
2.8 - the \emph{Isabelle/Isar Reference Manual}~\cite{isabelle-isar-ref}
2.9 - and the \emph{Isabelle Reference Manual}~\cite{isabelle-ref} for the
2.10 - actual Isabelle commands and related functions.
2.11 + interfaces as seen from a system oriented view. See also the
2.12 + \emph{Isabelle/Isar Reference Manual}~\cite{isabelle-isar-ref} for
2.13 + the actual Isabelle input language and related concepts.
2.14
2.15 - \medskip The Isabelle system environment emerges from a few general
2.16 - concepts.
2.17 + \medskip The Isabelle system environment provides the following
2.18 + basic infrastructure to integrate tools smoothly.
2.19
2.20 \begin{enumerate}
2.21
2.22 - \item The \emph{Isabelle settings} mechanism provides environment
2.23 - variables to all Isabelle programs (including tools and user
2.24 - interfaces).
2.25 + \item The \emph{Isabelle settings} mechanism provides process
2.26 + environment variables to all Isabelle executables (including tools
2.27 + and user interfaces).
2.28
2.29 \item The \emph{raw Isabelle process} (@{executable_ref
2.30 "isabelle-process"}) runs logic sessions either interactively or in
2.31 @@ -33,11 +32,6 @@
2.32 user interfaces etc. Such tools automatically benefit from the
2.33 settings mechanism.
2.34
2.35 - \item The \emph{Isabelle interface wrapper} (@{executable_ref
2.36 - "isabelle-interface"}) provides some abstraction over the actual
2.37 - user interface to be used. The de-facto standard interface for
2.38 - Isabelle is Proof~General \cite{proofgeneral}.
2.39 -
2.40 \end{enumerate}
2.41 *}
2.42
2.43 @@ -256,11 +250,6 @@
2.44 derives an individual directory for temporary files. The default is
2.45 somewhere in @{verbatim "/tmp"}.
2.46
2.47 - \item[@{setting_def ISABELLE_INTERFACE}] is an identifier that
2.48 - specifies the actual user interface that the capital @{executable
2.49 - Isabelle} or @{executable "isabelle-interface"} should invoke. See
2.50 - \secref{sec:interface} for more details.
2.51 -
2.52 \end{description}
2.53 *}
2.54
2.55 @@ -480,41 +469,4 @@
2.56 by @{verbatim "isabelle make"} alone.
2.57 *}
2.58
2.59 -
2.60 -section {* The Isabelle interface wrapper \label{sec:interface} *}
2.61 -
2.62 -text {*
2.63 - Isabelle is a generic theorem prover, even w.r.t.\ its user
2.64 - interface. The @{executable_def Isabelle} (or @{executable_def
2.65 - "isabelle-interface"}) executable provides a uniform way for
2.66 - end-users to invoke a certain interface; which one to start is
2.67 - determined by the @{setting_ref ISABELLE_INTERFACE} setting
2.68 - variable, which should give a full path specification to the actual
2.69 - executable.
2.70 -
2.71 - Presently, the most prominent Isabelle interface is Proof
2.72 - General~\cite{proofgeneral}\index{user interface!Proof General}.
2.73 - The Proof General distribution includes an interface wrapper script
2.74 - for the regular Isar toplevel, see @{verbatim
2.75 - "ProofGeneral/isar/interface"}. The canonical settings for
2.76 - Isabelle/Isar are as follows:
2.77 -
2.78 -\begin{ttbox}
2.79 -ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
2.80 -PROOFGENERAL_OPTIONS=""
2.81 -\end{ttbox}
2.82 -
2.83 - Thus @{executable Isabelle} would automatically invoke Emacs with
2.84 - proper setup of the Proof General Lisp packages. There are some
2.85 - options available, such as @{verbatim "-l"} for passing the logic
2.86 - image to be used by default, or @{verbatim "-m"} to tune the
2.87 - standard print mode.
2.88 -
2.89 - \medskip Note that the world may be also seen the other way round:
2.90 - Emacs may be started first (with proper setup of Proof General
2.91 - mode), and @{executable "isabelle-process"} run from within. This
2.92 - requires further Emacs Lisp configuration, see the Proof General
2.93 - documentation \cite{proofgeneral} for more information.
2.94 -*}
2.95 -
2.96 end
2.97 \ No newline at end of file
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/doc-src/System/Thy/Interfaces.thy Sun Nov 30 14:03:46 2008 +0100
3.3 @@ -0,0 +1,77 @@
3.4 +(* $Id$ *)
3.5 +
3.6 +theory Interfaces
3.7 +imports Pure
3.8 +begin
3.9 +
3.10 +chapter {* User interfaces *}
3.11 +
3.12 +section {* Plain TTY interaction \label{sec:tool-tty} *}
3.13 +
3.14 +text {*
3.15 + The @{tool_def tty} tool runs the Isabelle process interactively
3.16 + within a plain terminal session:
3.17 +\begin{ttbox}
3.18 +Usage: tty [OPTIONS]
3.19 +
3.20 + Options are:
3.21 + -l NAME logic image name (default ISABELLE_LOGIC)
3.22 + -m MODE add print mode for output
3.23 + -p NAME line editor program name (default ISABELLE_LINE_EDITOR)
3.24 +
3.25 + Run Isabelle process with plain tty interaction, and optional line editor.
3.26 +\end{ttbox}
3.27 +
3.28 + The @{verbatim "-l"} option specifies the logic image. The
3.29 + @{verbatim "-m"} option specifies additional print modes. The The
3.30 + @{verbatim "-p"} option specifies an alternative line editor (such
3.31 + as the @{executable_def rlwrap} wrapper for GNU readline); the
3.32 + fall-back is to use raw standard input.
3.33 +
3.34 + Regular interaction is via the standard Isabelle/Isar toplevel loop.
3.35 + The Isar command @{command exit} drops out into the raw ML system,
3.36 + which is occasionally useful for low-level debugging. Invoking @{ML
3.37 + Isar.loop}~@{verbatim "();"} in ML will return to the Isar toplevel.
3.38 +*}
3.39 +
3.40 +
3.41 +section {* Proof General / Emacs *}
3.42 +
3.43 +text {*
3.44 + The @{tool_def emacs} tool invokes a version of Emacs and Proof
3.45 + General within the regular Isabelle settings environment
3.46 + (\secref{sec:settings}). This is more robust than starting Emacs
3.47 + separately, loading the Proof General lisp files, and then
3.48 + attempting to start Isabelle with dynamic @{setting PATH} lookup
3.49 + etc.
3.50 +
3.51 + The actual interface script is part of the Proof General
3.52 + distribution~\cite{proofgeneral}; its usage depends on the
3.53 + particular version. There are some options available, such as
3.54 + @{verbatim "-l"} for passing the logic image to be used by default,
3.55 + or @{verbatim "-m"} to tune the standard print mode. The following
3.56 + Isabelle settings are particularly important for Proof General:
3.57 +
3.58 + \begin{description}
3.59 +
3.60 + \item[@{setting_def PROOFGENERAL_HOME}] points to the main
3.61 + installation directory of the Proof General distribution. The
3.62 + default settings try to locate this in a number of standard places,
3.63 + notably @{verbatim "$ISABELLE_HOME/contrib/ProofGeneral"}.
3.64 +
3.65 + \item[@{setting_def PROOFGENERAL_OPTIONS}] is implicitly prefixed to
3.66 + the command line of any invocation of the Proof General @{verbatim
3.67 + interface} script.
3.68 +
3.69 + \item[@{setting_def XSYMBOL_INSTALLFONTS}] may contain a small shell
3.70 + script to install the X11 fonts required for the X-Symbols mode of
3.71 + Proof General. This is only relevant if the X11 display server runs
3.72 + on a different machine than the Emacs application, with a different
3.73 + file-system view on the Proof General installation. Under most
3.74 + circumstances Proof General is able to refer to the font files that
3.75 + are part of its distribution.
3.76 +
3.77 + \end{description}
3.78 +*}
3.79 +
3.80 +end
3.81 \ No newline at end of file
4.1 --- a/doc-src/System/Thy/Misc.thy Sun Nov 30 14:03:45 2008 +0100
4.2 +++ b/doc-src/System/Thy/Misc.thy Sun Nov 30 14:03:46 2008 +0100
4.3 @@ -12,46 +12,6 @@
4.4 *}
4.5
4.6
4.7 -section {* The Proof General / Emacs interface *}
4.8 -
4.9 -text {*
4.10 - The @{tool_def emacs} tool invokes a version of Emacs and Proof
4.11 - General within the regular Isabelle settings environment
4.12 - (\secref{sec:settings}). This is more robust than starting Emacs
4.13 - separately, loading the Proof General lisp files, and then
4.14 - attempting to start Isabelle with dynamic @{setting PATH} lookup
4.15 - etc.
4.16 -
4.17 - The actual interface script is part of the Proof General
4.18 - distribution~\cite{proofgeneral}; its usage depends on the
4.19 - particular version. There are some options available, such as
4.20 - @{verbatim "-l"} for passing the logic image to be used by default,
4.21 - or @{verbatim "-m"} to tune the standard print mode. The following
4.22 - Isabelle settings are particularly important for Proof General:
4.23 -
4.24 - \begin{description}
4.25 -
4.26 - \item[@{setting_def PROOFGENERAL_HOME}] points to the main
4.27 - installation directory of the Proof General distribution. The
4.28 - default settings try to locate this in a number of standard places,
4.29 - notably @{verbatim "$ISABELLE_HOME/contrib/ProofGeneral"}.
4.30 -
4.31 - \item[@{setting_def PROOFGENERAL_OPTIONS}] is implicitly prefixed to
4.32 - the command line of any invocation of the Proof General @{verbatim
4.33 - interface} script.
4.34 -
4.35 - \item[@{setting_def XSYMBOL_INSTALLFONTS}] may contain a small shell
4.36 - script to install the X11 fonts required for the X-Symbols mode of
4.37 - Proof General. This is only relevant if the X11 display server runs
4.38 - on a different machine than the Emacs application, with a different
4.39 - file-system view on the Proof General installation. Under most
4.40 - circumstances Proof General is able to refer to the font files that
4.41 - are part of its distribution.
4.42 -
4.43 - \end{description}
4.44 -*}
4.45 -
4.46 -
4.47 section {* Displaying documents *}
4.48
4.49 text {*
4.50 @@ -294,30 +254,6 @@
4.51 *}
4.52
4.53
4.54 -section {* Run Isabelle with plain tty interaction \label{sec:tool-tty} *}
4.55 -
4.56 -text {*
4.57 - The @{tool_def tty} utility runs the Isabelle process interactively
4.58 - within a plain terminal session:
4.59 -\begin{ttbox}
4.60 -Usage: tty [OPTIONS]
4.61 -
4.62 - Options are:
4.63 - -l NAME logic image name (default ISABELLE_LOGIC)
4.64 - -m MODE add print mode for output
4.65 - -p NAME line editor program name (default ISABELLE_LINE_EDITOR)
4.66 -
4.67 - Run Isabelle process with plain tty interaction, and optional line editor.
4.68 -\end{ttbox}
4.69 -
4.70 - The @{verbatim "-l"} option specifies the logic image. The
4.71 - @{verbatim "-m"} option specifies additional print modes. The The
4.72 - @{verbatim "-p"} option specifies an alternative line editor (such
4.73 - as the @{executable_def rlwrap} wrapper for GNU readline); the
4.74 - fall-back is to use raw standard input.
4.75 -*}
4.76 -
4.77 -
4.78 section {* Remove awkward symbol names from theory sources *}
4.79
4.80 text {*
5.1 --- a/doc-src/System/Thy/ROOT.ML Sun Nov 30 14:03:45 2008 +0100
5.2 +++ b/doc-src/System/Thy/ROOT.ML Sun Nov 30 14:03:46 2008 +0100
5.3 @@ -5,5 +5,6 @@
5.4 use "../../antiquote_setup.ML";
5.5
5.6 use_thy "Basics";
5.7 +use_thy "Interfaces";
5.8 use_thy "Presentation";
5.9 use_thy "Misc";
6.1 --- a/doc-src/System/Thy/document/Basics.tex Sun Nov 30 14:03:45 2008 +0100
6.2 +++ b/doc-src/System/Thy/document/Basics.tex Sun Nov 30 14:03:46 2008 +0100
6.3 @@ -26,19 +26,18 @@
6.4 %
6.5 \begin{isamarkuptext}%
6.6 This manual describes Isabelle together with related tools and user
6.7 - interfaces as seen from an outside (system oriented) view. See also
6.8 - the \emph{Isabelle/Isar Reference Manual}~\cite{isabelle-isar-ref}
6.9 - and the \emph{Isabelle Reference Manual}~\cite{isabelle-ref} for the
6.10 - actual Isabelle commands and related functions.
6.11 + interfaces as seen from a system oriented view. See also the
6.12 + \emph{Isabelle/Isar Reference Manual}~\cite{isabelle-isar-ref} for
6.13 + the actual Isabelle input language and related concepts.
6.14
6.15 - \medskip The Isabelle system environment emerges from a few general
6.16 - concepts.
6.17 + \medskip The Isabelle system environment provides the following
6.18 + basic infrastructure to integrate tools smoothly.
6.19
6.20 \begin{enumerate}
6.21
6.22 - \item The \emph{Isabelle settings} mechanism provides environment
6.23 - variables to all Isabelle programs (including tools and user
6.24 - interfaces).
6.25 + \item The \emph{Isabelle settings} mechanism provides process
6.26 + environment variables to all Isabelle executables (including tools
6.27 + and user interfaces).
6.28
6.29 \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
6.30 batch mode. In particular, this view abstracts over the invocation
6.31 @@ -50,10 +49,6 @@
6.32 user interfaces etc. Such tools automatically benefit from the
6.33 settings mechanism.
6.34
6.35 - \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
6.36 - user interface to be used. The de-facto standard interface for
6.37 - Isabelle is Proof~General \cite{proofgeneral}.
6.38 -
6.39 \end{enumerate}%
6.40 \end{isamarkuptext}%
6.41 \isamarkuptrue%
6.42 @@ -262,10 +257,6 @@
6.43 derives an individual directory for temporary files. The default is
6.44 somewhere in \verb|/tmp|.
6.45
6.46 - \item[\indexdef{}{setting}{ISABELLE\_INTERFACE}\hypertarget{setting.ISABELLE-INTERFACE}{\hyperlink{setting.ISABELLE-INTERFACE}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}INTERFACE}}}}}] is an identifier that
6.47 - 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
6.48 - \secref{sec:interface} for more details.
6.49 -
6.50 \end{description}%
6.51 \end{isamarkuptext}%
6.52 \isamarkuptrue%
6.53 @@ -492,43 +483,6 @@
6.54 \end{isamarkuptext}%
6.55 \isamarkuptrue%
6.56 %
6.57 -\isamarkupsection{The Isabelle interface wrapper \label{sec:interface}%
6.58 -}
6.59 -\isamarkuptrue%
6.60 -%
6.61 -\begin{isamarkuptext}%
6.62 -Isabelle is a generic theorem prover, even w.r.t.\ its user
6.63 - 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
6.64 - end-users to invoke a certain interface; which one to start is
6.65 - determined by the \indexref{}{setting}{ISABELLE\_INTERFACE}\hyperlink{setting.ISABELLE-INTERFACE}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}INTERFACE}}}} setting
6.66 - variable, which should give a full path specification to the actual
6.67 - executable.
6.68 -
6.69 - Presently, the most prominent Isabelle interface is Proof
6.70 - General~\cite{proofgeneral}\index{user interface!Proof General}.
6.71 - The Proof General distribution includes an interface wrapper script
6.72 - for the regular Isar toplevel, see \verb|ProofGeneral/isar/interface|. The canonical settings for
6.73 - Isabelle/Isar are as follows:
6.74 -
6.75 -\begin{ttbox}
6.76 -ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
6.77 -PROOFGENERAL_OPTIONS=""
6.78 -\end{ttbox}
6.79 -
6.80 - Thus \hyperlink{executable.Isabelle}{\mbox{\isa{\isatt{Isabelle}}}} would automatically invoke Emacs with
6.81 - proper setup of the Proof General Lisp packages. There are some
6.82 - options available, such as \verb|-l| for passing the logic
6.83 - image to be used by default, or \verb|-m| to tune the
6.84 - standard print mode.
6.85 -
6.86 - \medskip Note that the world may be also seen the other way round:
6.87 - Emacs may be started first (with proper setup of Proof General
6.88 - mode), and \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}} run from within. This
6.89 - requires further Emacs Lisp configuration, see the Proof General
6.90 - documentation \cite{proofgeneral} for more information.%
6.91 -\end{isamarkuptext}%
6.92 -\isamarkuptrue%
6.93 -%
6.94 \isadelimtheory
6.95 %
6.96 \endisadelimtheory
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/doc-src/System/Thy/document/Interfaces.tex Sun Nov 30 14:03:46 2008 +0100
7.3 @@ -0,0 +1,115 @@
7.4 +%
7.5 +\begin{isabellebody}%
7.6 +\def\isabellecontext{Interfaces}%
7.7 +%
7.8 +\isadelimtheory
7.9 +\isanewline
7.10 +\isanewline
7.11 +%
7.12 +\endisadelimtheory
7.13 +%
7.14 +\isatagtheory
7.15 +\isacommand{theory}\isamarkupfalse%
7.16 +\ Interfaces\isanewline
7.17 +\isakeyword{imports}\ Pure\isanewline
7.18 +\isakeyword{begin}%
7.19 +\endisatagtheory
7.20 +{\isafoldtheory}%
7.21 +%
7.22 +\isadelimtheory
7.23 +%
7.24 +\endisadelimtheory
7.25 +%
7.26 +\isamarkupchapter{User interfaces%
7.27 +}
7.28 +\isamarkuptrue%
7.29 +%
7.30 +\isamarkupsection{Plain TTY interaction \label{sec:tool-tty}%
7.31 +}
7.32 +\isamarkuptrue%
7.33 +%
7.34 +\begin{isamarkuptext}%
7.35 +The \indexdef{}{tool}{tty}\hypertarget{tool.tty}{\hyperlink{tool.tty}{\mbox{\isa{\isatt{tty}}}}} tool runs the Isabelle process interactively
7.36 + within a plain terminal session:
7.37 +\begin{ttbox}
7.38 +Usage: tty [OPTIONS]
7.39 +
7.40 + Options are:
7.41 + -l NAME logic image name (default ISABELLE_LOGIC)
7.42 + -m MODE add print mode for output
7.43 + -p NAME line editor program name (default ISABELLE_LINE_EDITOR)
7.44 +
7.45 + Run Isabelle process with plain tty interaction, and optional line editor.
7.46 +\end{ttbox}
7.47 +
7.48 + The \verb|-l| option specifies the logic image. The
7.49 + \verb|-m| option specifies additional print modes. The The
7.50 + \verb|-p| option specifies an alternative line editor (such
7.51 + as the \indexdef{}{executable}{rlwrap}\hypertarget{executable.rlwrap}{\hyperlink{executable.rlwrap}{\mbox{\isa{\isatt{rlwrap}}}}} wrapper for GNU readline); the
7.52 + fall-back is to use raw standard input.
7.53 +
7.54 + Regular interaction is via the standard Isabelle/Isar toplevel loop.
7.55 + The Isar command \hyperlink{command.exit}{\mbox{\isa{\isacommand{exit}}}} drops out into the raw ML system,
7.56 + which is occasionally useful for low-level debugging. Invoking \verb|Isar.loop|~\verb|();| in ML will return to the Isar toplevel.%
7.57 +\end{isamarkuptext}%
7.58 +\isamarkuptrue%
7.59 +%
7.60 +\isamarkupsection{Proof General / Emacs%
7.61 +}
7.62 +\isamarkuptrue%
7.63 +%
7.64 +\begin{isamarkuptext}%
7.65 +The \indexdef{}{tool}{emacs}\hypertarget{tool.emacs}{\hyperlink{tool.emacs}{\mbox{\isa{\isatt{emacs}}}}} tool invokes a version of Emacs and Proof
7.66 + General within the regular Isabelle settings environment
7.67 + (\secref{sec:settings}). This is more robust than starting Emacs
7.68 + separately, loading the Proof General lisp files, and then
7.69 + attempting to start Isabelle with dynamic \hyperlink{setting.PATH}{\mbox{\isa{\isatt{PATH}}}} lookup
7.70 + etc.
7.71 +
7.72 + The actual interface script is part of the Proof General
7.73 + distribution~\cite{proofgeneral}; its usage depends on the
7.74 + particular version. There are some options available, such as
7.75 + \verb|-l| for passing the logic image to be used by default,
7.76 + or \verb|-m| to tune the standard print mode. The following
7.77 + Isabelle settings are particularly important for Proof General:
7.78 +
7.79 + \begin{description}
7.80 +
7.81 + \item[\indexdef{}{setting}{PROOFGENERAL\_HOME}\hypertarget{setting.PROOFGENERAL-HOME}{\hyperlink{setting.PROOFGENERAL-HOME}{\mbox{\isa{\isatt{PROOFGENERAL{\isacharunderscore}HOME}}}}}] points to the main
7.82 + installation directory of the Proof General distribution. The
7.83 + default settings try to locate this in a number of standard places,
7.84 + notably \verb|$ISABELLE_HOME/contrib/ProofGeneral|.
7.85 +
7.86 + \item[\indexdef{}{setting}{PROOFGENERAL\_OPTIONS}\hypertarget{setting.PROOFGENERAL-OPTIONS}{\hyperlink{setting.PROOFGENERAL-OPTIONS}{\mbox{\isa{\isatt{PROOFGENERAL{\isacharunderscore}OPTIONS}}}}}] is implicitly prefixed to
7.87 + the command line of any invocation of the Proof General \verb|interface| script.
7.88 +
7.89 + \item[\indexdef{}{setting}{XSYMBOL\_INSTALLFONTS}\hypertarget{setting.XSYMBOL-INSTALLFONTS}{\hyperlink{setting.XSYMBOL-INSTALLFONTS}{\mbox{\isa{\isatt{XSYMBOL{\isacharunderscore}INSTALLFONTS}}}}}] may contain a small shell
7.90 + script to install the X11 fonts required for the X-Symbols mode of
7.91 + Proof General. This is only relevant if the X11 display server runs
7.92 + on a different machine than the Emacs application, with a different
7.93 + file-system view on the Proof General installation. Under most
7.94 + circumstances Proof General is able to refer to the font files that
7.95 + are part of its distribution.
7.96 +
7.97 + \end{description}%
7.98 +\end{isamarkuptext}%
7.99 +\isamarkuptrue%
7.100 +%
7.101 +\isadelimtheory
7.102 +%
7.103 +\endisadelimtheory
7.104 +%
7.105 +\isatagtheory
7.106 +\isacommand{end}\isamarkupfalse%
7.107 +%
7.108 +\endisatagtheory
7.109 +{\isafoldtheory}%
7.110 +%
7.111 +\isadelimtheory
7.112 +%
7.113 +\endisadelimtheory
7.114 +\end{isabellebody}%
7.115 +%%% Local Variables:
7.116 +%%% mode: latex
7.117 +%%% TeX-master: "root"
7.118 +%%% End:
8.1 --- a/doc-src/System/Thy/document/Misc.tex Sun Nov 30 14:03:45 2008 +0100
8.2 +++ b/doc-src/System/Thy/document/Misc.tex Sun Nov 30 14:03:46 2008 +0100
8.3 @@ -30,47 +30,6 @@
8.4 \end{isamarkuptext}%
8.5 \isamarkuptrue%
8.6 %
8.7 -\isamarkupsection{The Proof General / Emacs interface%
8.8 -}
8.9 -\isamarkuptrue%
8.10 -%
8.11 -\begin{isamarkuptext}%
8.12 -The \indexdef{}{tool}{emacs}\hypertarget{tool.emacs}{\hyperlink{tool.emacs}{\mbox{\isa{\isatt{emacs}}}}} tool invokes a version of Emacs and Proof
8.13 - General within the regular Isabelle settings environment
8.14 - (\secref{sec:settings}). This is more robust than starting Emacs
8.15 - separately, loading the Proof General lisp files, and then
8.16 - attempting to start Isabelle with dynamic \hyperlink{setting.PATH}{\mbox{\isa{\isatt{PATH}}}} lookup
8.17 - etc.
8.18 -
8.19 - The actual interface script is part of the Proof General
8.20 - distribution~\cite{proofgeneral}; its usage depends on the
8.21 - particular version. There are some options available, such as
8.22 - \verb|-l| for passing the logic image to be used by default,
8.23 - or \verb|-m| to tune the standard print mode. The following
8.24 - Isabelle settings are particularly important for Proof General:
8.25 -
8.26 - \begin{description}
8.27 -
8.28 - \item[\indexdef{}{setting}{PROOFGENERAL\_HOME}\hypertarget{setting.PROOFGENERAL-HOME}{\hyperlink{setting.PROOFGENERAL-HOME}{\mbox{\isa{\isatt{PROOFGENERAL{\isacharunderscore}HOME}}}}}] points to the main
8.29 - installation directory of the Proof General distribution. The
8.30 - default settings try to locate this in a number of standard places,
8.31 - notably \verb|$ISABELLE_HOME/contrib/ProofGeneral|.
8.32 -
8.33 - \item[\indexdef{}{setting}{PROOFGENERAL\_OPTIONS}\hypertarget{setting.PROOFGENERAL-OPTIONS}{\hyperlink{setting.PROOFGENERAL-OPTIONS}{\mbox{\isa{\isatt{PROOFGENERAL{\isacharunderscore}OPTIONS}}}}}] is implicitly prefixed to
8.34 - the command line of any invocation of the Proof General \verb|interface| script.
8.35 -
8.36 - \item[\indexdef{}{setting}{XSYMBOL\_INSTALLFONTS}\hypertarget{setting.XSYMBOL-INSTALLFONTS}{\hyperlink{setting.XSYMBOL-INSTALLFONTS}{\mbox{\isa{\isatt{XSYMBOL{\isacharunderscore}INSTALLFONTS}}}}}] may contain a small shell
8.37 - script to install the X11 fonts required for the X-Symbols mode of
8.38 - Proof General. This is only relevant if the X11 display server runs
8.39 - on a different machine than the Emacs application, with a different
8.40 - file-system view on the Proof General installation. Under most
8.41 - circumstances Proof General is able to refer to the font files that
8.42 - are part of its distribution.
8.43 -
8.44 - \end{description}%
8.45 -\end{isamarkuptext}%
8.46 -\isamarkuptrue%
8.47 -%
8.48 \isamarkupsection{Displaying documents%
8.49 }
8.50 \isamarkuptrue%
8.51 @@ -329,32 +288,6 @@
8.52 \end{isamarkuptext}%
8.53 \isamarkuptrue%
8.54 %
8.55 -\isamarkupsection{Run Isabelle with plain tty interaction \label{sec:tool-tty}%
8.56 -}
8.57 -\isamarkuptrue%
8.58 -%
8.59 -\begin{isamarkuptext}%
8.60 -The \indexdef{}{tool}{tty}\hypertarget{tool.tty}{\hyperlink{tool.tty}{\mbox{\isa{\isatt{tty}}}}} utility runs the Isabelle process interactively
8.61 - within a plain terminal session:
8.62 -\begin{ttbox}
8.63 -Usage: tty [OPTIONS]
8.64 -
8.65 - Options are:
8.66 - -l NAME logic image name (default ISABELLE_LOGIC)
8.67 - -m MODE add print mode for output
8.68 - -p NAME line editor program name (default ISABELLE_LINE_EDITOR)
8.69 -
8.70 - Run Isabelle process with plain tty interaction, and optional line editor.
8.71 -\end{ttbox}
8.72 -
8.73 - The \verb|-l| option specifies the logic image. The
8.74 - \verb|-m| option specifies additional print modes. The The
8.75 - \verb|-p| option specifies an alternative line editor (such
8.76 - as the \indexdef{}{executable}{rlwrap}\hypertarget{executable.rlwrap}{\hyperlink{executable.rlwrap}{\mbox{\isa{\isatt{rlwrap}}}}} wrapper for GNU readline); the
8.77 - fall-back is to use raw standard input.%
8.78 -\end{isamarkuptext}%
8.79 -\isamarkuptrue%
8.80 -%
8.81 \isamarkupsection{Remove awkward symbol names from theory sources%
8.82 }
8.83 \isamarkuptrue%
9.1 --- a/doc-src/System/system.tex Sun Nov 30 14:03:45 2008 +0100
9.2 +++ b/doc-src/System/system.tex Sun Nov 30 14:03:46 2008 +0100
9.3 @@ -20,7 +20,7 @@
9.4 \title{\includegraphics[scale=0.5]{isabelle} \\[4ex] The Isabelle System Manual}
9.5
9.6 \author{\emph{Makarius Wenzel} and \emph{Stefan Berghofer} \\
9.7 - TU München}
9.8 + TU M\"unchen}
9.9
9.10 \makeindex
9.11
9.12 @@ -31,6 +31,7 @@
9.13 \pagenumbering{roman} \tableofcontents \clearfirst
9.14
9.15 \input{Thy/document/Basics.tex}
9.16 +\input{Thy/document/Interfaces.tex}
9.17 \input{Thy/document/Presentation.tex}
9.18 \input{Thy/document/Misc.tex}
9.19