--- a/bin/isabelle-process Thu Nov 29 17:38:41 2007 +0100
+++ b/bin/isabelle-process Thu Nov 29 18:09:36 2007 +0100
@@ -36,6 +36,7 @@
echo " -e MLTEXT pass MLTEXT to the ML session"
echo " -f pass 'Session.finish();' to the ML session"
echo " -m MODE add print mode for output"
+ echo " -p echo ISABELLE_PID on startup"
echo " -q non-interactive session"
echo " -r open heap file read-only"
echo " -u pass 'use\"ROOT.ML\";' to the ML session"
@@ -67,11 +68,12 @@
COMPRESS=""
MLTEXT=""
MODES=""
+ECHOPID=""
TERMINATE=""
READONLY=""
NOWRITE=""
-while getopts "XCIPSce:fm:qruw" OPT
+while getopts "XCIPSce:fm:pqruw" OPT
do
case "$OPT" in
C)
@@ -105,6 +107,9 @@
MODES="\"$OPTARG\", $MODES"
fi
;;
+ p)
+ ECHOPID=true
+ ;;
q)
TERMINATE=true
;;
@@ -227,6 +232,8 @@
export INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE \
ISABELLE_PID ISABELLE_TMP
+[ -n "$ECHOPID" ] && echo "ISABELLE_PID=$ISABELLE_PID"
+
if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then
"$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM"
else
--- a/doc-src/System/basics.tex Thu Nov 29 17:38:41 2007 +0100
+++ b/doc-src/System/basics.tex Thu Nov 29 18:09:36 2007 +0100
@@ -286,6 +286,7 @@
-e MLTEXT pass MLTEXT to the ML session
-f pass 'Session.finish();' to the ML session
-m MODE add print mode for output
+ -p echo ISABELLE_PID on startup
-q non-interactive session
-r open heap file read-only
-u pass 'use"ROOT.ML";' to the ML session
@@ -362,6 +363,12 @@
by disabling some critical operations, notably runtime compilation and
evaluation of ML source code.
+\medskip The \texttt{-p} option echos the \texttt{ISABELLE_PID}
+variable on startup, which is the operating system identifier of the
+Isabelle process group. This enables to control the process later on,
+e.g.\ sending an interrupt signal like this: \verb,kill -INT -,$pid$
+(the $pid$ is negated here to address the whole process group).
+
\subsection*{Examples}