# HG changeset patch
# User wenzelm
# Date 1427898278 -7200
# Node ID 2a616319c17161aa1adb4c36ae119bb90d0264ae
# Parent  9ce6970504552e153ad0c9367e94ac4ca517abd8
added isabelle build option -x, to exclude sessions;

diff -r 9ce697050455 -r 2a616319c171 NEWS
--- a/NEWS	Wed Apr 01 15:41:08 2015 +0200
+++ b/NEWS	Wed Apr 01 16:24:38 2015 +0200
@@ -396,7 +396,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 option -k.
+* The Isabelle tool "build" provides new options -k and -x.
 
 
 
diff -r 9ce697050455 -r 2a616319c171 lib/Tools/build
--- a/lib/Tools/build	Wed Apr 01 15:41:08 2015 +0200
+++ b/lib/Tools/build	Wed Apr 01 16:24:38 2015 +0200
@@ -40,6 +40,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
   echo "  Build and manage Isabelle sessions, depending on implicit"
   show_settings "  "
@@ -75,8 +76,9 @@
 eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)"
 SYSTEM_MODE=false
 VERBOSE=false
+declare -a EXCLUDE_SESSIONS=()
 
-while getopts "D:Rabcd:g:j:k:lno:sv" OPT
+while getopts "D:Rabcd:g:j:k:lno:svx:" OPT
 do
   case "$OPT" in
     D)
@@ -122,6 +124,9 @@
     v)
       VERBOSE="true"
       ;;
+    x)
+      EXCLUDE_SESSIONS["${#EXCLUDE_SESSIONS[@]}"]="$OPTARG"
+      ;;
     \?)
       usage
       ;;
@@ -151,7 +156,7 @@
   "$LIST_FILES" "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \
   "${INCLUDE_DIRS[@]}" $'\n' "${SELECT_DIRS[@]}" $'\n' \
   "${SESSION_GROUPS[@]}" $'\n' "${CHECK_KEYWORDS[@]}" $'\n' \
-  "${BUILD_OPTIONS[@]}" $'\n' "$@"
+  "${BUILD_OPTIONS[@]}" $'\n' "${EXCLUDE_SESSIONS[@]}" $'\n' "$@"
 RC="$?"
 
 if [ "$NO_BUILD" = false -a "$VERBOSE" = true ]; then
diff -r 9ce697050455 -r 2a616319c171 src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Wed Apr 01 15:41:08 2015 +0200
+++ b/src/Doc/System/Sessions.thy	Wed Apr 01 16:24:38 2015 +0200
@@ -290,6 +290,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
 
   Build and manage Isabelle sessions, depending on implicit
   ISABELLE_BUILD_OPTIONS="..."
@@ -322,6 +323,10 @@
   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
+  sessions to be excluded. All descendents of excluded sessions are removed
+  from the selection as specified above.
+
   \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
diff -r 9ce697050455 -r 2a616319c171 src/Pure/PIDE/batch_session.scala
--- a/src/Pure/PIDE/batch_session.scala	Wed Apr 01 15:41:08 2015 +0200
+++ b/src/Pure/PIDE/batch_session.scala	Wed Apr 01 16:24:38 2015 +0200
@@ -19,7 +19,7 @@
     session: String): Batch_Session =
   {
     val (_, session_tree) =
-      Build.find_sessions(options, dirs).selection(false, false, Nil, List(session))
+      Build.find_sessions(options, dirs).selection(sessions = List(session))
     val session_info = session_tree(session)
     val parent_session =
       session_info.parent getOrElse error("No parent session for " + quote(session))
diff -r 9ce697050455 -r 2a616319c171 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Apr 01 15:41:08 2015 +0200
+++ b/src/Pure/Tools/build.scala	Wed Apr 01 16:24:38 2015 +0200
@@ -162,12 +162,18 @@
     def apply(name: String): Session_Info = graph.get_node(name)
     def isDefinedAt(name: String): Boolean = graph.defined(name)
 
-    def selection(requirements: Boolean, all_sessions: Boolean,
-      session_groups: List[String], sessions: List[String]): (List[String], Session_Tree) =
+    def selection(
+      requirements: Boolean = false,
+      all_sessions: Boolean = false,
+      session_groups: List[String] = Nil,
+      exclude_sessions: List[String] = Nil,
+      sessions: List[String] = Nil): (List[String], Session_Tree) =
     {
-      val bad_sessions = sessions.filterNot(isDefinedAt(_))
+      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 pre_selected =
       {
         if (all_sessions) graph.keys
@@ -179,7 +185,8 @@
             if info.select || select(name) || apply(name).groups.exists(select_group)
           } yield name).toList
         }
-      }
+      }.filterNot(excluded)
+
       val selected =
         if (requirements) (graph.all_preds(pre_selected).toSet -- pre_selected).toList
         else pre_selected
@@ -533,7 +540,7 @@
     dirs: List[Path],
     sessions: List[String]): Deps =
   {
-    val (_, tree) = find_sessions(options, dirs = dirs).selection(false, false, Nil, sessions)
+    val (_, tree) = find_sessions(options, dirs = dirs).selection(sessions = sessions)
     dependencies(inlined_files = inlined_files, tree = tree)
   }
 
@@ -758,13 +765,14 @@
     no_build: Boolean = false,
     system_mode: Boolean = false,
     verbose: Boolean = false,
+    exclude_sessions: List[String] = Nil,
     sessions: List[String] = Nil): Map[String, Int] =
   {
     /* session tree and dependencies */
 
     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, sessions)
+      full_tree.selection(requirements, all_sessions, session_groups, exclude_sessions, sessions)
 
     val deps = dependencies(progress, true, verbose, list_files, check_keywords, selected_tree)
 
@@ -1010,12 +1018,13 @@
     no_build: Boolean = false,
     system_mode: Boolean = false,
     verbose: Boolean = false,
+    exclude_sessions: List[String] = Nil,
     sessions: List[String] = Nil): Int =
   {
     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, sessions)
+      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)
 
     val rc = (0 /: results)({ case (rc1, (_, rc2)) => rc1 max rc2 })
     if (rc != 0 && (verbose || !no_build)) {
@@ -1043,15 +1052,15 @@
           Properties.Value.Boolean(no_build) ::
           Properties.Value.Boolean(system_mode) ::
           Properties.Value.Boolean(verbose) ::
-          Command_Line.Chunks(
-              dirs, select_dirs, session_groups, check_keywords, build_options, sessions) =>
+          Command_Line.Chunks(dirs, select_dirs, session_groups, check_keywords,
+              build_options, 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,
-                verbose, sessions)
+                verbose, exclude_sessions, sessions)
             }
         case _ => error("Bad arguments:\n" + cat_lines(args))
       }