allow to exclude session groups;

--- a/NEWS	Fri Apr 17 09:56:12 2015 +0200
+++ b/NEWS	Fri Apr 17 11:28:57 2015 +0200
@@ -449,7 +449,7 @@
 * The Isabelle tool "update_cartouches" changes theory files to use
 cartouches instead of old-style {* verbatim *} or `alt_string` tokens.
 
-* The Isabelle tool "build" provides new options -k and -x.
+* The Isabelle tool "build" provides new options -X, -k, -x.
 
 * Discontinued old-fashioned "codegen" tool. Code generation can always
 be externally triggered using an appropriate ROOT file plus a

--- a/lib/Tools/build	Fri Apr 17 09:56:12 2015 +0200
+++ b/lib/Tools/build	Fri Apr 17 11:28:57 2015 +0200
@@ -28,6 +28,7 @@
   echo "  Options are:"
   echo "    -D DIR       include session directory and select its sessions"
   echo "    -R           operate on requirements of selected sessions"
+  echo "    -X NAME      exclude sessions from group NAME and all descendants"
   echo "    -a           select all sessions"
   echo "    -b           build heap images"
   echo "    -c           clean build"
@@ -40,7 +41,7 @@
   echo "    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)"
   echo "    -s           system build mode: produce output in ISABELLE_HOME"
   echo "    -v           verbose"
-  echo "    -x SESSION   exclude SESSION and all its descendants"
+  echo "    -x NAME      exclude session NAME and all descendants"
   echo
   echo "  Build and manage Isabelle sessions, depending on implicit"
   show_settings "  "
@@ -64,6 +65,7 @@
 
 declare -a SELECT_DIRS=()
 REQUIREMENTS=false
+declare -a EXCLUDE_SESSION_GROUPS=()
 ALL_SESSIONS=false
 BUILD_HEAP=false
 CLEAN_BUILD=false
@@ -78,7 +80,7 @@
 VERBOSE=false
 declare -a EXCLUDE_SESSIONS=()
 
-while getopts "D:Rabcd:g:j:k:lno:svx:" OPT
+while getopts "D:RX:abcd:g:j:k:lno:svx:" OPT
 do
   case "$OPT" in
     D)
@@ -87,6 +89,9 @@
     R)
       REQUIREMENTS="true"
       ;;
+    X)
+      EXCLUDE_SESSION_GROUPS["${#EXCLUDE_SESSION_GROUPS[@]}"]="$OPTARG"
+      ;;
     a)
       ALL_SESSIONS="true"
       ;;
@@ -156,7 +161,8 @@
   "$LIST_FILES" "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \
   "${INCLUDE_DIRS[@]}" $'\n' "${SELECT_DIRS[@]}" $'\n' \
   "${SESSION_GROUPS[@]}" $'\n' "${CHECK_KEYWORDS[@]}" $'\n' \
-  "${BUILD_OPTIONS[@]}" $'\n' "${EXCLUDE_SESSIONS[@]}" $'\n' "$@"
+  "${BUILD_OPTIONS[@]}" $'\n' "${EXCLUDE_SESSION_GROUPS[@]}" $'\n' \
+  "${EXCLUDE_SESSIONS[@]}" $'\n' "$@"
 RC="$?"
 
 if [ "$NO_BUILD" = false -a "$VERBOSE" = true ]; then

--- a/src/Doc/System/Sessions.thy	Fri Apr 17 09:56:12 2015 +0200
+++ b/src/Doc/System/Sessions.thy	Fri Apr 17 11:28:57 2015 +0200
@@ -278,6 +278,7 @@
   Options are:
     -D DIR       include session directory and select its sessions
     -R           operate on requirements of selected sessions
+    -X NAME      exclude sessions from group NAME and all descendants
     -a           select all sessions
     -b           build heap images
     -c           clean build
@@ -290,7 +291,7 @@
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -s           system build mode: produce output in ISABELLE_HOME
     -v           verbose
-    -x SESSION   exclude SESSION and all its descendants
+    -x NAME      exclude session NAME and all descendants
 
   Build and manage Isabelle sessions, depending on implicit
   ISABELLE_BUILD_OPTIONS="..."
@@ -323,9 +324,11 @@
   The build tool takes session dependencies into account: the set of
   selected sessions is completed by including all ancestors.
 
-  \medskip One or more options @{verbatim "-x"}~@{text SESSION} specify
+  \medskip One or more options @{verbatim "-x"}~@{text NAME} specify
   sessions to be excluded. All descendents of excluded sessions are removed
-  from the selection as specified above.
+  from the selection as specified above. Option @{verbatim "-X"} is
+  analogous to this, but excluded sessions are specified by session group
+  membership.
 
   \medskip Option @{verbatim "-R"} reverses the selection in the sense
   that it refers to its requirements: all ancestor sessions excluding

--- a/src/Pure/Tools/build.scala	Fri Apr 17 09:56:12 2015 +0200
+++ b/src/Pure/Tools/build.scala	Fri Apr 17 11:28:57 2015 +0200
@@ -165,15 +165,26 @@
     def selection(
       requirements: Boolean = false,
       all_sessions: Boolean = false,
+      exclude_session_groups: List[String] = Nil,
+      exclude_sessions: List[String] = Nil,
       session_groups: List[String] = Nil,
-      exclude_sessions: List[String] = Nil,
       sessions: List[String] = Nil): (List[String], Session_Tree) =
     {
       val bad_sessions =
         SortedSet((exclude_sessions ::: sessions).filterNot(isDefinedAt(_)): _*).toList
       if (bad_sessions.nonEmpty) error("Undefined session(s): " + commas_quote(bad_sessions))
 
-      val excluded = graph.all_succs(exclude_sessions).toSet
+      val excluded =
+      {
+        val exclude_group = exclude_session_groups.toSet
+        val exclude_group_sessions =
+          (for {
+            (name, (info, _)) <- graph.iterator
+            if apply(name).groups.exists(exclude_group)
+          } yield name).toList
+        graph.all_succs(exclude_group_sessions ::: exclude_sessions).toSet
+      }
+
       val pre_selected =
       {
         if (all_sessions) graph.keys
@@ -751,6 +762,7 @@
     clean_build: Boolean = false,
     dirs: List[Path] = Nil,
     select_dirs: List[Path] = Nil,
+    exclude_session_groups: List[String] = Nil,
     session_groups: List[String] = Nil,
     max_jobs: Int = 1,
     list_files: Boolean = false,
@@ -765,7 +777,8 @@
 
     val full_tree = find_sessions(options.int("completion_limit") = 0, dirs, select_dirs)
     val (selected, selected_tree) =
-      full_tree.selection(requirements, all_sessions, session_groups, exclude_sessions, sessions)
+      full_tree.selection(requirements, all_sessions,
+        exclude_session_groups, exclude_sessions, session_groups, sessions)
 
     val deps = dependencies(progress, true, verbose, list_files, check_keywords, selected_tree)
 
@@ -1004,6 +1017,7 @@
     clean_build: Boolean = false,
     dirs: List[Path] = Nil,
     select_dirs: List[Path] = Nil,
+    exclude_session_groups: List[String] = Nil,
     session_groups: List[String] = Nil,
     max_jobs: Int = 1,
     list_files: Boolean = false,
@@ -1016,8 +1030,8 @@
   {
     val results =
       build_results(options, progress, requirements, all_sessions, build_heap, clean_build,
-        dirs, select_dirs, session_groups, max_jobs, list_files, check_keywords,
-        no_build, system_mode, verbose, exclude_sessions, sessions)
+        dirs, select_dirs, exclude_session_groups, session_groups, max_jobs, list_files,
+        check_keywords, no_build, system_mode, verbose, exclude_sessions, sessions)
 
     val rc = (0 /: results)({ case (rc1, (_, rc2)) => rc1 max rc2 })
     if (rc != 0 && (verbose || !no_build)) {
@@ -1046,13 +1060,13 @@
           Properties.Value.Boolean(system_mode) ::
           Properties.Value.Boolean(verbose) ::
           Command_Line.Chunks(dirs, select_dirs, session_groups, check_keywords,
-              build_options, exclude_sessions, sessions) =>
+              build_options, exclude_session_groups, exclude_sessions, sessions) =>
             val options = (Options.init() /: build_options)(_ + _)
             val progress = new Console_Progress(verbose)
             progress.interrupt_handler {
               build(options, progress, requirements, all_sessions, build_heap, clean_build,
-                dirs.map(Path.explode(_)), select_dirs.map(Path.explode(_)), session_groups,
-                max_jobs, list_files, check_keywords.toSet, no_build, system_mode,
+                dirs.map(Path.explode(_)), select_dirs.map(Path.explode(_)), exclude_session_groups,
+                session_groups, max_jobs, list_files, check_keywords.toSet, no_build, system_mode,
                 verbose, exclude_sessions, sessions)
             }
         case _ => error("Bad arguments:\n" + cat_lines(args))
@@ -1116,4 +1130,3 @@
         Markup.LOADING_THEORY -> loading_theory _)
   }
 }
-