1.1 --- a/doc-src/System/Thy/Sessions.thy	Sun Aug 05 20:11:32 2012 +0200
     1.2 +++ b/doc-src/System/Thy/Sessions.thy	Sun Aug 05 21:57:25 2012 +0200
     1.3 @@ -197,6 +197,13 @@
     1.4    command line.  Each such directory may contain a session
     1.5    \texttt{ROOT} file with several session specifications.
     1.6  
     1.7 +  Any session root directory may refer recursively to further
     1.8 +  directories of the same kind, by listing them in a catalog file
     1.9 +  @{verbatim "ROOTS"} line-by-line.  This helps to organize large
    1.10 +  collections of session specifications, or to make @{verbatim "-d"}
    1.11 +  command line options persistent (say within @{verbatim
    1.12 +  "$ISABELLE_HOME_USER/ROOTS"}).
    1.13 +
    1.14    \medskip The subset of sessions to be managed is determined via
    1.15    individual @{text "SESSIONS"} given as command-line arguments, or
    1.16    session groups that are given via one or more options @{verbatim

     2.1 --- a/doc-src/System/Thy/document/Sessions.tex	Sun Aug 05 20:11:32 2012 +0200
     2.2 +++ b/doc-src/System/Thy/document/Sessions.tex	Sun Aug 05 21:57:25 2012 +0200
     2.3 @@ -313,6 +313,12 @@
     2.4    command line.  Each such directory may contain a session
     2.5    \texttt{ROOT} file with several session specifications.
     2.6  
     2.7 +  Any session root directory may refer recursively to further
     2.8 +  directories of the same kind, by listing them in a catalog file
     2.9 +  \verb|ROOTS| line-by-line.  This helps to organize large
    2.10 +  collections of session specifications, or to make \verb|-d|
    2.11 +  command line options persistent (say within \verb|$ISABELLE_HOME_USER/ROOTS|).
    2.12 +
    2.13    \medskip The subset of sessions to be managed is determined via
    2.14    individual \isa{{\isaliteral{22}{\isachardoublequote}}SESSIONS{\isaliteral{22}{\isachardoublequote}}} given as command-line arguments, or
    2.15    session groups that are given via one or more options \verb|-g|~\isa{{\isaliteral{22}{\isachardoublequote}}NAME{\isaliteral{22}{\isachardoublequote}}}.  Option \verb|-a| selects all sessions.

     3.1 --- a/src/Pure/System/build.scala	Sun Aug 05 20:11:32 2012 +0200
     3.2 +++ b/src/Pure/System/build.scala	Sun Aug 05 21:57:25 2012 +0200
     3.3 @@ -100,7 +100,7 @@
     3.4      {
     3.5        val graph1 =
     3.6          (Graph.string[Session_Info] /: infos) {
     3.7 -          case (graph, (name, info)) => graph.new_node(name, info)
     3.8 +          case (graph, (name, info)) =>
     3.9              if (graph.defined(name))
    3.10                error("Duplicate session " + quote(name) + Position.str_of(info.pos))
    3.11              else graph.new_node(name, info)
    3.12 @@ -214,20 +214,52 @@
    3.13    /* find sessions within certain directories */
    3.14  
    3.15    private val ROOT = Path.explode("ROOT")
    3.16 +  private val ROOTS = Path.explode("ROOTS")
    3.17  
    3.18 -  private def is_session_dir(dir: Path): Boolean = (dir + ROOT).is_file
    3.19 +  private def is_session_dir(dir: Path): Boolean =
    3.20 +    (dir + ROOT).is_file || (dir + ROOTS).is_file
    3.21  
    3.22 -  private def sessions_root(options: Options, dir: Path): List[(String, Session_Info)] =
    3.23 -  {
    3.24 -    val root = dir + ROOT
    3.25 -    if (root.is_file) Parser.parse_entries(dir + ROOT).map(session_info(options, dir, _))
    3.26 -    else error("Bad session root file: " + root.toString)
    3.27 -  }
    3.28 +  private def check_session_dir(dir: Path): Path =
    3.29 +    if (is_session_dir(dir)) dir
    3.30 +    else error("Bad session root directory: " + dir.toString)
    3.31  
    3.32    def find_sessions(options: Options, more_dirs: List[Path]): Session_Tree =
    3.33    {
    3.34 -    val dirs = Isabelle_System.components().filter(is_session_dir(_)) ::: more_dirs
    3.35 -    Session_Tree(dirs.map(sessions_root(options, _)).flatten)
    3.36 +    def find_dir(dir: Path): List[(String, Session_Info)] = find_root(dir) ::: find_roots(dir)
    3.37 +
    3.38 +    def find_root(dir: Path): List[(String, Session_Info)] =
    3.39 +    {
    3.40 +      val root = dir + ROOT
    3.41 +      if (root.is_file) Parser.parse_entries(root).map(session_info(options, dir, _))
    3.42 +      else Nil
    3.43 +    }
    3.44 +
    3.45 +    def find_roots(dir: Path): List[(String, Session_Info)] =
    3.46 +    {
    3.47 +      val roots = dir + ROOTS
    3.48 +      if (roots.is_file) {
    3.49 +        for {
    3.50 +          line <- split_lines(File.read(roots))
    3.51 +          if !(line == "" || line.startsWith("#"))
    3.52 +          dir1 =
    3.53 +            try { check_session_dir(dir + Path.explode(line)) }
    3.54 +            catch {
    3.55 +              case ERROR(msg) =>
    3.56 +                error(msg + "\nThe error(s) above occurred in session catalog " + roots.toString)
    3.57 +            }
    3.58 +          info <- find_dir(dir1)
    3.59 +        } yield info
    3.60 +      }
    3.61 +      else Nil
    3.62 +    }
    3.63 +
    3.64 +    Session_Tree(
    3.65 +      for {
    3.66 +        dir <-
    3.67 +          Isabelle_System.components().filter(is_session_dir(_)) :::
    3.68 +          more_dirs.map(check_session_dir(_))
    3.69 +        info <- find_dir(dir)
    3.70 +      } yield info)
    3.71    }
    3.72  
    3.73