# HG changeset patch
# User wenzelm
# Date 1196356176 -3600
# Node ID dc960d760052981d2578b2865795ba1bc26cbd16
# Parent  fe14c6857f1dd4a64e65f446ab7353552cf7669a
isabelle-process: option -p echos ISABELLE_PID;

diff -r fe14c6857f1d -r dc960d760052 bin/isabelle-process
--- 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
diff -r fe14c6857f1d -r dc960d760052 doc-src/System/basics.tex
--- 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}