--- a/doc-src/System/basics.tex Wed Mar 08 17:41:40 2000 +0100
+++ b/doc-src/System/basics.tex Wed Mar 08 17:44:53 2000 +0100
@@ -55,7 +55,7 @@
not required.}
-\subsection{Creating the environment}
+\subsection{Building the environment}
Whenever any of the Isabelle executables is run, their settings environment is
built as follows.
@@ -207,14 +207,15 @@
\section{Isabelle proper --- \texttt{isabelle}}
-The \ttindex{isabelle} executable runs logic sessions --- either interactively
-or in batch mode. It provides an abstraction over the underlying {\ML} system,
-and over the actual heap file locations. Its usage is:
+The \ttindex{isabelle} executable runs bare-bones logic sessions --- either
+interactively or in batch mode. It provides an abstraction over the underlying
+{\ML} system, and over the actual heap file locations. Its usage is:
\begin{ttbox}
Usage: isabelle [OPTIONS] [INPUT] [OUTPUT]
Options are:
-I startup Isar interaction mode
+ -c tell ML system to compress output image
-e MLTEXT pass MLTEXT to the ML session
-m MODE add print mode for output
-q non-interactive session
@@ -254,6 +255,11 @@
terminating. Thus subsequent invocations cause the logic image to be
read-only automatically.
+\medskip The \texttt{-c} option tells the underlying ML system to compress the
+output heap (fully transparently). On Poly/ML for example, the image is
+garbage collected and all values maximally shared, resulting in up to 50\%
+less disk space consumption.
+
\medskip Using the \texttt{-e} option, arbitrary {\ML} code may be passed to
the Isabelle session from the command line. Multiple \texttt{-e}'s are
evaluated in the given order. Strange things may happen when errorneous {\ML}