--- a/doc-src/System/basics.tex Tue Jan 16 00:22:43 2001 +0100
+++ b/doc-src/System/basics.tex Tue Jan 16 00:23:14 2001 +0100
@@ -218,6 +218,7 @@
-P startup Proof General interaction mode
-c tell ML system to compress output image
-e MLTEXT pass MLTEXT to the ML session
+ -f pass 'Session.finish();' to the ML session
-m MODE add print mode for output
-q non-interactive session
-r open heap file read-only
@@ -272,8 +273,10 @@
code is provided. Also make sure that the {\ML} commands are terminated
properly by semicolon.
-\medskip The \texttt{-u} option is a shortcut for \texttt{-e}, passing
-``\texttt{use"ROOT.ML";}'' to the {\ML} session.
+\medskip The \texttt{-u} option is a shortcut for \texttt{-e} passing
+``\texttt{use"ROOT.ML";}'' to the {\ML} session. The \texttt{-f} option
+passes ``\texttt{Session.finish();}'', which is intended mainly for
+administrative purposes.
\medskip The \texttt{-m} option adds identifiers of print modes to be made
active for this session. Typically, this is used by some user interface, e.g.\
--- a/src/Pure/mk Tue Jan 16 00:22:43 2001 +0100
+++ b/src/Pure/mk Tue Jan 16 00:23:14 2001 +0100
@@ -93,7 +93,7 @@
"$ISABELLE" $COPY \
-e "val ml_system = \"$ML_SYSTEM\";" \
-e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \
- -c -q -w RAW_ML_SYSTEM Pure > "$LOG" 2>&1
+ -f -c -q -w RAW_ML_SYSTEM Pure > "$LOG" 2>&1
RC="$?"
else
ITEM="RAW"
@@ -102,7 +102,7 @@
"$ISABELLE" $COPY \
-e "val ml_system = \"$ML_SYSTEM\";" \
- -e "use\"$COMPAT\" handle _ => exit 1;;" \
+ -e "use\"$COMPAT\" handle _ => exit 1;" \
-q -w RAW_ML_SYSTEM RAW > "$LOG" 2>&1
RC="$?"
fi