src/Doc/System/Sessions.thy
changeset 49131 aa1e2ba3c697
parent 48985 5386df44a037
child 50406 c28753665b8e
--- a/src/Doc/System/Sessions.thy	Tue Sep 04 18:49:40 2012 +0200
+++ b/src/Doc/System/Sessions.thy	Tue Sep 04 20:45:43 2012 +0200
@@ -183,6 +183,7 @@
 
   Options are:
     -D DIR       include session directory and select its sessions
+    -R           operate on requirements of selected sessions
     -a           select all sessions
     -b           build heap images
     -c           clean build
@@ -227,6 +228,12 @@
   The build tool takes session dependencies into account: the set of
   selected sessions is completed by including all ancestors.
 
+  \medskip Option @{verbatim "-R"} reverses the selection in the sense
+  that it refers to its requirements: all ancestor sessions excluding
+  the original selection.  This allows to prepare the stage for some
+  build process with different options, before running the main build
+  itself (without option @{verbatim "-R"}).
+
   \medskip Option @{verbatim "-D"} is similar to @{verbatim "-d"}, but
   selects all sessions that are defined in the given directories.
 
@@ -319,6 +326,12 @@
 \begin{ttbox}
 isabelle build -D '$AFP'
 \end{ttbox}
+
+  \smallskip Inform about the status of all sessions required for AFP,
+  without building anything yet:
+\begin{ttbox}
+isabelle build -D '$AFP' -R -v -n
+\end{ttbox}
 *}
 
 end