# HG changeset patch
# User wenzelm
# Date 1506856051 -7200
# Node ID 2edc0c42c883967df343d3942d51f384b887cfd7
# Parent  14889103646959cc83de6df01cbef2c0240d54b6
option -B for "isabelle build" and "isabelle imports";

diff -r 148891036469 -r 2edc0c42c883 NEWS
--- a/NEWS	Sun Oct 01 12:28:52 2017 +0200
+++ b/NEWS	Sun Oct 01 13:07:31 2017 +0200
@@ -27,6 +27,9 @@
 * Windows and Cygwin is for x86_64 only. Old 32bit platform support has
 been discontinued.
 
+* Command-line tool "isabelle build" supports option -B for base
+sessions: all descendants are included.
+
 
 New in Isabelle2017 (October 2017)
 ----------------------------------
diff -r 148891036469 -r 2edc0c42c883 src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Sun Oct 01 12:28:52 2017 +0200
+++ b/src/Doc/System/Sessions.thy	Sun Oct 01 13:07:31 2017 +0200
@@ -280,6 +280,7 @@
 \<open>Usage: isabelle build [OPTIONS] [SESSIONS ...]
 
   Options are:
+    -B NAME      include session NAME and all descendants
     -D DIR       include session directory and select its sessions
     -N           cyclic shuffling of NUMA CPU nodes (performance tuning)
     -R           operate on requirements of selected sessions
@@ -329,6 +330,10 @@
   completed by including all ancestors.
 
   \<^medskip>
+  One or more options \<^verbatim>\<open>-B\<close>~\<open>NAME\<close> specify base sessions. All descendants
+  are included.
+
+  \<^medskip>
   One or more options \<^verbatim>\<open>-x\<close>~\<open>NAME\<close> specify sessions to be excluded. All
   descendents of excluded sessions are removed from the selection as specified
   above. Option \<^verbatim>\<open>-X\<close> is analogous to this, but excluded sessions are
@@ -450,6 +455,7 @@
 \<open>Usage: isabelle imports [OPTIONS] [SESSIONS ...]
 
   Options are:
+    -B NAME      include session NAME and all descendants
     -D DIR       include session directory and select its sessions
     -I           operation: report potential session imports
     -M           operation: Mercurial repository check for theory files
@@ -469,7 +475,7 @@
 
   \<^medskip>
   The selection of sessions and session directories works as for @{tool build}
-  via options \<^verbatim>\<open>-D\<close>, \<^verbatim>\<open>-R\<close>, \<^verbatim>\<open>-X\<close>, \<^verbatim>\<open>-a\<close>, \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-g\<close>, \<^verbatim>\<open>-x\<close> (see
+  via options \<^verbatim>\<open>-B\<close>, \<^verbatim>\<open>-D\<close>, \<^verbatim>\<open>-R\<close>, \<^verbatim>\<open>-X\<close>, \<^verbatim>\<open>-a\<close>, \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-g\<close>, \<^verbatim>\<open>-x\<close> (see
   \secref{sec:tool-build}).
 
   \<^medskip>
diff -r 148891036469 -r 2edc0c42c883 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sun Oct 01 12:28:52 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Sun Oct 01 13:07:31 2017 +0200
@@ -368,6 +368,7 @@
   sealed case class Selection(
     requirements: Boolean = false,
     all_sessions: Boolean = false,
+    base_sessions: List[String] = Nil,
     exclude_session_groups: List[String] = Nil,
     exclude_sessions: List[String] = Nil,
     session_groups: List[String] = Nil,
@@ -377,6 +378,7 @@
       Selection(
         requirements = requirements || other.requirements,
         all_sessions = all_sessions || other.all_sessions,
+        base_sessions = Library.merge(base_sessions, other.base_sessions),
         exclude_session_groups = Library.merge(exclude_session_groups, other.exclude_session_groups),
         exclude_sessions = Library.merge(exclude_sessions, other.exclude_sessions),
         session_groups = Library.merge(session_groups, other.session_groups),
@@ -385,8 +387,10 @@
     def apply(graph: Graph[String, Info]): (List[String], Graph[String, Info]) =
     {
       val bad_sessions =
-        SortedSet((exclude_sessions ::: sessions).filterNot(graph.defined(_)): _*).toList
-      if (bad_sessions.nonEmpty) error("Undefined session(s): " + commas_quote(bad_sessions))
+        SortedSet((base_sessions ::: exclude_sessions ::: sessions).
+          filterNot(graph.defined(_)): _*).toList
+      if (bad_sessions.nonEmpty)
+        error("Undefined session(s): " + commas_quote(bad_sessions))
 
       val excluded =
       {
@@ -404,7 +408,7 @@
         if (all_sessions) graph.keys
         else {
           val select_group = session_groups.toSet
-          val select = sessions.toSet
+          val select = sessions.toSet ++ graph.all_succs(base_sessions)
           (for {
             (name, (info, _)) <- graph.iterator
             if info.select || select(name) || graph.get_node(name).groups.exists(select_group)
diff -r 148891036469 -r 2edc0c42c883 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sun Oct 01 12:28:52 2017 +0200
+++ b/src/Pure/Tools/build.scala	Sun Oct 01 13:07:31 2017 +0200
@@ -357,6 +357,7 @@
     pide: Boolean = false,
     requirements: Boolean = false,
     all_sessions: Boolean = false,
+    base_sessions: List[String] = Nil,
     exclude_session_groups: List[String] = Nil,
     exclude_sessions: List[String] = Nil,
     session_groups: List[String] = Nil,
@@ -371,7 +372,7 @@
 
     val (selected, selected_sessions) =
       full_sessions.selection(
-          Sessions.Selection(requirements, all_sessions, exclude_session_groups,
+          Sessions.Selection(requirements, all_sessions, base_sessions, exclude_session_groups,
             exclude_sessions, session_groups, sessions) ++ selection)
 
     val deps =
@@ -627,6 +628,7 @@
   {
     val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
 
+    var base_sessions: List[String] = Nil
     var select_dirs: List[Path] = Nil
     var numa_shuffling = false
     var pide = false
@@ -650,6 +652,7 @@
 Usage: isabelle build [OPTIONS] [SESSIONS ...]
 
   Options are:
+    -B NAME      include session NAME and all descendants
     -D DIR       include session directory and select its sessions
     -N           cyclic shuffling of NUMA CPU nodes (performance tuning)
     -P           build via PIDE protocol
@@ -672,6 +675,7 @@
   Build and manage Isabelle sessions, depending on implicit settings:
 
 """ + Library.prefix_lines("  ", Build_Log.Settings.show()) + "\n",
+      "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
       "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
       "N" -> (_ => numa_shuffling = true),
       "P" -> (_ => pide = true),
@@ -722,6 +726,7 @@
           pide = pide,
           requirements = requirements,
           all_sessions = all_sessions,
+          base_sessions = base_sessions,
           exclude_session_groups = exclude_session_groups,
           exclude_sessions = exclude_sessions,
           session_groups = session_groups,
diff -r 148891036469 -r 2edc0c42c883 src/Pure/Tools/imports.scala
--- a/src/Pure/Tools/imports.scala	Sun Oct 01 12:28:52 2017 +0200
+++ b/src/Pure/Tools/imports.scala	Sun Oct 01 13:07:31 2017 +0200
@@ -215,6 +215,7 @@
   val isabelle_tool =
     Isabelle_Tool("imports", "maintain theory imports wrt. session structure", args =>
     {
+      var base_sessions: List[String] = Nil
       var select_dirs: List[Path] = Nil
       var operation_imports = false
       var operation_repository_files = false
@@ -233,6 +234,7 @@
 Usage: isabelle imports [OPTIONS] [SESSIONS ...]
 
   Options are:
+    -B NAME      include session NAME and all descendants
     -D DIR       include session directory and select its sessions
     -I           operation: report potential session imports
     -M           operation: Mercurial repository check for theory files
@@ -250,6 +252,7 @@
   Maintain theory imports wrt. session structure. At least one operation
   needs to be specified (see options -I -M -U).
 """,
+      "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
       "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
       "I" -> (_ => operation_imports = true),
       "M" -> (_ => operation_repository_files = true),
@@ -269,7 +272,7 @@
         getopts.usage()
 
       val selection =
-        Sessions.Selection(requirements, all_sessions, exclude_session_groups,
+        Sessions.Selection(requirements, all_sessions, base_sessions, exclude_session_groups,
           exclude_sessions, session_groups, sessions)
 
       val progress = new Console_Progress(verbose = verbose)