added build option -D: include session directory and select its sessions;

--- a/doc-src/System/Thy/Sessions.thy	Wed Aug 08 14:45:40 2012 +0200
+++ b/doc-src/System/Thy/Sessions.thy	Wed Aug 08 15:58:40 2012 +0200
@@ -192,10 +192,11 @@
 Usage: isabelle build [OPTIONS] [SESSIONS ...]
 
   Options are:
+    -D DIR       include session directory and select its sessions
     -a           select all sessions
     -b           build heap images
     -c           clean build
-    -d DIR       include session directory with ROOT file
+    -d DIR       include session directory
     -g NAME      select session group NAME
     -j INT       maximum number of parallel jobs (default 1)
     -n           no build -- test dependencies only
@@ -235,6 +236,9 @@
   The build tool takes session dependencies into account: the set of
   selected sessions is completed by including all ancestors.
 
+  \medskip Option @{verbatim "-D"} is similar to @{verbatim "-d"}, but
+  selects all sessions that are defined in the given directories.
+
   \medskip The build process depends on additional options
   (\secref{sec:system-options}) that are passed to the prover
   eventually.  The settings variable @{setting_ref
@@ -315,6 +319,13 @@
 \begin{ttbox}
 isabelle build -a -n -c
 \end{ttbox}
+
+  \smallskip Build all sessions from some other directory hierarchy,
+  according to the settings variable @{verbatim "AFP"} that happens to
+  be defined inside the Isabelle environment:
+\begin{ttbox}
+isabelle build -D '$AFP'
+\end{ttbox}
 *}
 
 

--- a/doc-src/System/Thy/document/Sessions.tex	Wed Aug 08 14:45:40 2012 +0200
+++ b/doc-src/System/Thy/document/Sessions.tex	Wed Aug 08 15:58:40 2012 +0200
@@ -308,10 +308,11 @@
 Usage: isabelle build [OPTIONS] [SESSIONS ...]
 
   Options are:
+    -D DIR       include session directory and select its sessions
     -a           select all sessions
     -b           build heap images
     -c           clean build
-    -d DIR       include session directory with ROOT file
+    -d DIR       include session directory
     -g NAME      select session group NAME
     -j INT       maximum number of parallel jobs (default 1)
     -n           no build -- test dependencies only
@@ -349,6 +350,9 @@
   The build tool takes session dependencies into account: the set of
   selected sessions is completed by including all ancestors.
 
+  \medskip Option \verb|-D| is similar to \verb|-d|, but
+  selects all sessions that are defined in the given directories.
+
   \medskip The build process depends on additional options
   (\secref{sec:system-options}) that are passed to the prover
   eventually.  The settings variable \indexref{}{setting}{ISABELLE\_BUILD\_OPTIONS}\hyperlink{setting.ISABELLE-BUILD-OPTIONS}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}BUILD{\isaliteral{5F}{\isacharunderscore}}OPTIONS}}}} allows to provide additional defaults, e.g.\
@@ -428,6 +432,13 @@
   \smallskip Clean all sessions without building anything:
 \begin{ttbox}
 isabelle build -a -n -c
+\end{ttbox}
+
+  \smallskip Build all sessions from some other directory hierarchy,
+  according to the settings variable \verb|AFP| that happens to
+  be defined inside the Isabelle environment:
+\begin{ttbox}
+isabelle build -D '$AFP'
 \end{ttbox}%
 \end{isamarkuptext}%
 \isamarkuptrue%

--- a/lib/Tools/build	Wed Aug 08 14:45:40 2012 +0200
+++ b/lib/Tools/build	Wed Aug 08 15:58:40 2012 +0200
@@ -26,10 +26,11 @@
   echo "Usage: isabelle $PRG [OPTIONS] [SESSIONS ...]"
   echo
   echo "  Options are:"
+  echo "    -D DIR       include session directory and select its sessions"
   echo "    -a           select all sessions"
   echo "    -b           build heap images"
   echo "    -c           clean build"
-  echo "    -d DIR       include session directory with ROOT file"
+  echo "    -d DIR       include session directory"
   echo "    -g NAME      select session group NAME"
   echo "    -j INT       maximum number of parallel jobs (default 1)"
   echo "    -n           no build -- test dependencies only"
@@ -57,10 +58,11 @@
 
 ## process command line
 
+declare -a SELECT_DIRS=()
 ALL_SESSIONS=false
 BUILD_HEAP=false
 CLEAN_BUILD=false
-declare -a MORE_DIRS=()
+declare -a INCLUDE_DIRS=()
 declare -a SESSION_GROUPS=()
 MAX_JOBS=1
 NO_BUILD=false
@@ -68,9 +70,12 @@
 SYSTEM_MODE=false
 VERBOSE=false
 
-while getopts "abcd:g:j:no:sv" OPT
+while getopts "D:abcd:g:j:no:sv" OPT
 do
   case "$OPT" in
+    D)
+      SELECT_DIRS["${#SELECT_DIRS[@]}"]="$OPTARG"
+      ;;
     a)
       ALL_SESSIONS="true"
       ;;
@@ -81,7 +86,7 @@
       CLEAN_BUILD="true"
       ;;
     d)
-      MORE_DIRS["${#MORE_DIRS[@]}"]="$OPTARG"
+      INCLUDE_DIRS["${#INCLUDE_DIRS[@]}"]="$OPTARG"
       ;;
     g)
       SESSION_GROUPS["${#SESSION_GROUPS[@]}"]="$OPTARG"
@@ -126,7 +131,8 @@
 "$ISABELLE_TOOL" java isabelle.Build \
   "$ALL_SESSIONS" "$BUILD_HEAP" "$CLEAN_BUILD" "$MAX_JOBS" \
   "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \
-  "${MORE_DIRS[@]}" $'\n' "${SESSION_GROUPS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"
+  "${SELECT_DIRS[@]}" $'\n' "${INCLUDE_DIRS[@]}" $'\n' \
+  "${SESSION_GROUPS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"
 RC="$?"
 
 if [ "$NO_BUILD" = false -a "$VERBOSE" = true ]; then

--- a/src/Pure/System/build.scala	Wed Aug 08 14:45:40 2012 +0200
+++ b/src/Pure/System/build.scala	Wed Aug 08 15:58:40 2012 +0200
@@ -35,6 +35,7 @@
 
   // internal version
   sealed case class Session_Info(
+    select: Boolean,
     pos: Position.T,
     groups: List[String],
     dir: Path,
@@ -47,7 +48,8 @@
 
   def is_pure(name: String): Boolean = name == "RAW" || name == "Pure"
 
-  def session_info(options: Options, dir: Path, entry: Session_Entry): (String, Session_Info) =
+  def session_info(options: Options, select: Boolean, dir: Path, entry: Session_Entry)
+      : (String, Session_Info) =
     try {
       if (entry.base_name == "") error("Bad session name")
 
@@ -80,7 +82,7 @@
         SHA1.digest((full_name, entry.parent, entry.options, entry.theories).toString)
 
       val info =
-        Session_Info(entry.pos, entry.groups, dir + path, entry.parent, entry.description,
+        Session_Info(select, entry.pos, entry.groups, dir + path, entry.parent, entry.description,
           session_options, theories, files, entry_digest)
 
       (full_name, info)
@@ -145,10 +147,12 @@
       {
         if (all_sessions) graph.keys.toList
         else {
-          val sel_group = session_groups.toSet
-          val sel = sessions.toSet
-            graph.keys.toList.filter(name =>
-              sel(name) || apply(name).groups.exists(sel_group)).toList
+          val select_group = session_groups.toSet
+          val select = sessions.toSet
+          (for {
+            (name, (info, _)) <- graph.entries
+            if info.select || select(name) || apply(name).groups.exists(select_group)
+          } yield name).toList
         }
       }
       val descendants = graph.all_succs(selected)
@@ -223,18 +227,19 @@
     if (is_session_dir(dir)) dir
     else error("Bad session root directory: " + dir.toString)
 
-  def find_sessions(options: Options, more_dirs: List[Path]): Session_Tree =
+  def find_sessions(options: Options, more_dirs: List[(Boolean, Path)]): Session_Tree =
   {
-    def find_dir(dir: Path): List[(String, Session_Info)] = find_root(dir) ::: find_roots(dir)
+    def find_dir(select: Boolean, dir: Path): List[(String, Session_Info)] =
+      find_root(select, dir) ::: find_roots(select, dir)
 
-    def find_root(dir: Path): List[(String, Session_Info)] =
+    def find_root(select: Boolean, dir: Path): List[(String, Session_Info)] =
     {
       val root = dir + ROOT
-      if (root.is_file) Parser.parse_entries(root).map(session_info(options, dir, _))
+      if (root.is_file) Parser.parse_entries(root).map(session_info(options, select, dir, _))
       else Nil
     }
 
-    def find_roots(dir: Path): List[(String, Session_Info)] =
+    def find_roots(select: Boolean, dir: Path): List[(String, Session_Info)] =
     {
       val roots = dir + ROOTS
       if (roots.is_file) {
@@ -247,18 +252,20 @@
               case ERROR(msg) =>
                 error(msg + "\nThe error(s) above occurred in session catalog " + roots.toString)
             }
-          info <- find_dir(dir1)
+          info <- find_dir(select, dir1)
         } yield info
       }
       else Nil
     }
 
+    val default_dirs = Isabelle_System.components().filter(is_session_dir(_)).map((false, _))
+
+    more_dirs foreach { case (_, dir) => check_session_dir(dir) }
+
     Session_Tree(
       for {
-        dir <-
-          Isabelle_System.components().filter(is_session_dir(_)) :::
-          more_dirs.map(check_session_dir(_))
-        info <- find_dir(dir)
+        (select, dir) <- default_dirs ::: more_dirs
+        info <- find_dir(select, dir)
       } yield info)
   }
 
@@ -529,7 +536,7 @@
     all_sessions: Boolean = false,
     build_heap: Boolean = false,
     clean_build: Boolean = false,
-    more_dirs: List[Path] = Nil,
+    more_dirs: List[(Boolean, Path)] = Nil,
     session_groups: List[String] = Nil,
     max_jobs: Int = 1,
     no_build: Boolean = false,
@@ -696,9 +703,12 @@
           Properties.Value.Boolean(no_build) ::
           Properties.Value.Boolean(system_mode) ::
           Properties.Value.Boolean(verbose) ::
-          Command_Line.Chunks(more_dirs, session_groups, build_options, sessions) =>
-            build(all_sessions, build_heap, clean_build, more_dirs.map(Path.explode),
-              session_groups, max_jobs, no_build, build_options, system_mode, verbose, sessions)
+          Command_Line.Chunks(select_dirs, include_dirs, session_groups, build_options, sessions) =>
+            val dirs =
+              select_dirs.map(d => (true, Path.explode(d))) :::
+              include_dirs.map(d => (false, Path.explode(d)))
+            build(all_sessions, build_heap, clean_build, dirs, session_groups,
+              max_jobs, no_build, build_options, system_mode, verbose, sessions)
         case _ => error("Bad arguments:\n" + cat_lines(args))
       }
     }