# HG changeset patch # User wenzelm # Date 940333551 -7200 # Node ID 01e6e05d208bb9175183514a7912dc26c51fb43c # Parent 52fb3667f7df8ec7a92e2fa2b7970eec87a86009 tuned; diff -r 52fb3667f7df -r 01e6e05d208b doc-src/System/basics.tex --- a/doc-src/System/basics.tex Mon Oct 18 19:43:18 1999 +0200 +++ b/doc-src/System/basics.tex Tue Oct 19 13:45:51 1999 +0200 @@ -4,7 +4,7 @@ \chapter{The Isabelle system environment} This manual describes Isabelle together with related tools and user interfaces -as seen from an outside, system oriented view. See also the \emph{Isabelle +as seen from an outside (system oriented) view. See also the \emph{Isabelle Reference Manual}~\cite{isabelle-ref} and the \emph{Isabelle Isar Reference Manual}~\cite{isabelle-isar-ref} for the actual Isabelle commands and related functions. @@ -48,17 +48,17 @@ In particular, we avoid the typical situation where prospective users of a software package are told to put several things into their shell startup -scripts, before being able to actually run it. Isabelle requires none such -administrative chores of its end-users --- the executables can be invoked -straight away. Occasionally, users would still want to put the Isabelle -\texttt{bin} directory into their shell's search path, but this is not -required. +scripts, before being able to actually run the program. Isabelle requires none +such administrative chores of its end-users --- the executables can be invoked +straight away.\footnote{Occasionally, users would still want to put the + Isabelle \texttt{bin} directory into their shell's search path, but this is + not required.} \subsection{Creating the environment} Whenever any of the Isabelle executables is run, their settings environment is -built as follows: +built as follows. \begin{enumerate} \item The special variable \settdx{ISABELLE_HOME} is determined automatically @@ -66,7 +66,7 @@ You should not try to set \texttt{ISABELLE_HOME} manually. Also note that the Isabelle executables either have to be run from their original location - in the distribution directory, or via the executable objects created via the + in the distribution directory, or via the executable objects created by the \texttt{install} utility (see \S\ref{sec:tool-install}). Just doing a plain copy of the \texttt{bin} files will not work! @@ -95,11 +95,10 @@ \end{enumerate} Note that settings files are actually full GNU bash scripts. So one may use -complex shell commands, such as \texttt{if} or \texttt{case} statements, to -set variables depending on the system architecture or other environment -variables. Such advanced features should be added only with great care, -though. In particular, external environment references should be kept at a -minimum. +complex shell commands, such as \texttt{if} or \texttt{case} statements to set +variables depending on the system architecture or other environment variables. +Such advanced features should be added only with great care, though. In +particular, external environment references should be kept at a minimum. \medskip A few variables are somewhat special: \begin{itemize} @@ -108,7 +107,7 @@ \texttt{isatool} executables, respectively. \item \settdx{ISABELLE_PATH} and \settdx{ISABELLE_OUTPUT} will have the {\ML} - system identifier (according to \texttt{ML_IDENTIFIER} automatically + system identifier (according to \texttt{ML_IDENTIFIER}) automatically appended to their values. \end{itemize} @@ -224,8 +223,8 @@ -w reset write permissions on OUTPUT INPUT (default "\$ISABELLE_LOGIC") and OUTPUT specify in/out heaps. - These are either names to be searched in the Isabelle path, or actual - file names (containing at least one /). + These are either names to be searched in the Isabelle path, or + actual file names (containing at least one /). If INPUT is "RAW_ML_SYSTEM", just start the bare bones ML system. \end{ttbox} Input files without path specifications are looked up in the @@ -361,8 +360,8 @@ \item \texttt{none} is just a pass-through to plain \texttt{isabelle}. Thus \texttt{Isabelle} basically becomes an alias for \texttt{isabelle}. -\item \texttt{xterm} refers to a simple xterm based interface which is part of - the Isabelle distribution. +\item \texttt{xterm} refers to a simple \textsl{xterm} based interface which + is part of the Isabelle distribution. \item \texttt{emacs} refers to David Aspinall's \emph{Isamode}\index{user interface!Isamode} for emacs. Isabelle just provides a wrapper for this, diff -r 52fb3667f7df -r 01e6e05d208b doc-src/System/misc.tex --- a/doc-src/System/misc.tex Mon Oct 18 19:43:18 1999 +0200 +++ b/doc-src/System/misc.tex Tue Oct 19 13:45:51 1999 +0200 @@ -34,8 +34,8 @@ Recursively find .ML files, expand shorthand goal commands. Also contracts uses of resolve_tac, dresolve_tac, eresolve_tac, - forward_tac, rewrite_goals_tac on 1-element lists; furthermore expands - tabs, which are forbidden in SML string constants. + forward_tac, rewrite_goals_tac on 1-element lists; furthermore + expands tabs, which are forbidden in SML string constants. Renames old versions of files by appending "~~". \end{ttbox} @@ -121,7 +121,8 @@ Usage: install [OPTIONS] Options are: - -d DISTDIR use DISTDIR as Isabelle distribution (default ISABELLE_HOME) + -d DISTDIR use DISTDIR as Isabelle distribution + (default ISABELLE_HOME) -k install KDE application icon on Desktop -p DIR install standalone binaries in DIR @@ -208,7 +209,6 @@ The arguments \texttt{ARGS} are just passed verbatim to each \texttt{make} invocation. - %%% Local Variables: %%% mode: latex %%% TeX-master: "system" diff -r 52fb3667f7df -r 01e6e05d208b doc-src/System/present.tex --- a/doc-src/System/present.tex Mon Oct 18 19:43:18 1999 +0200 +++ b/doc-src/System/present.tex Tue Oct 19 13:45:51 1999 +0200 @@ -324,7 +324,7 @@ -\section{Managing logic sessions --- \texttt{isatool usedir}} \label{sec:tool-usedir} +\section{Managing Isabelle logic sessions --- \texttt{isatool usedir}} \label{sec:tool-usedir} The \tooldx{usedir} utility builds object-logic images, or runs example sessions based on existing logics. Its usage is: @@ -332,7 +332,6 @@ Usage: usedir LOGIC NAME Options are: - -B build mode with THIS_IS_ISABELLE_BUILD indication -P PATH set path for remote theory browsing information -b build mode (output heap image, using current dir) -d FORMAT build document as FORMAT (default false) @@ -364,11 +363,7 @@ image \texttt{LOGIC} and output to \texttt{NAME}, as provided on the command line. This will be a batch session, running \texttt{ROOT.ML} from the current directory and then quitting. It is assumed that \texttt{ROOT.ML} contains all -{\ML} commands required to build the logic. The \texttt{-B} option is like -\texttt{-b}, but also indicates \texttt{THIS_IS_ISABELLE_BUILD=true} via the -process environment. This usually causes the \texttt{ISABELLE\_OUTPUT} and -\texttt{ISABELLE_BROWSER_INFO} settings to refer to some location within the -Isabelle distribution directory, rather than the user's home directory. +{\ML} commands required to build the logic. In example mode, \texttt{usedir} runs a read-only session of \texttt{LOGIC} and automatically runs \texttt{ROOT.ML} from within directory \texttt{NAME}. @@ -405,7 +400,6 @@ object-logics as a model for your own developments. For example, see \texttt{src/FOL/IsaMakefile}. - %%% Local Variables: %%% mode: latex %%% TeX-master: "system"