doc-src/System/Thy/Sessions.thy
changeset 48684 9170e10c651e
parent 48683 eeb4480b5877
child 48693 ceeea46bdeba
--- a/doc-src/System/Thy/Sessions.thy	Sun Aug 05 20:11:32 2012 +0200
+++ b/doc-src/System/Thy/Sessions.thy	Sun Aug 05 21:57:25 2012 +0200
@@ -197,6 +197,13 @@
   command line.  Each such directory may contain a session
   \texttt{ROOT} file with several session specifications.
 
+  Any session root directory may refer recursively to further
+  directories of the same kind, by listing them in a catalog file
+  @{verbatim "ROOTS"} line-by-line.  This helps to organize large
+  collections of session specifications, or to make @{verbatim "-d"}
+  command line options persistent (say within @{verbatim
+  "$ISABELLE_HOME_USER/ROOTS"}).
+
   \medskip The subset of sessions to be managed is determined via
   individual @{text "SESSIONS"} given as command-line arguments, or
   session groups that are given via one or more options @{verbatim