# HG changeset patch
# User wenzelm
# Date 1533149921 -7200
# Node ID c14a2cc9b5efbc945cad1e3c6ecdc4c5ebab7b0d
# Parent  76e339ef60e3dc14e0a85d1cf1f891ab45a19cb0
isabelle build options -c -x -B refer to imports_graph;

diff -r 76e339ef60e3 -r c14a2cc9b5ef NEWS
--- a/NEWS	Wed Aug 01 19:48:58 2018 +0200
+++ b/NEWS	Wed Aug 01 20:58:41 2018 +0200
@@ -473,6 +473,11 @@
   - option -S: only observe changes of sources, not heap images
   - option -f: forces a fresh build
 
+* Command-line tool "isabelle build" options -c -x -B refer to
+descendants wrt. the session parent or import graph. Subtle
+INCOMPATIBILITY: options -c -x used to refer to the session parent graph
+only.
+
 * Command-line tool "isabelle build" takes "condition" options with the
 corresponding environment values into account, when determining the
 up-to-date status of a session.
diff -r 76e339ef60e3 -r c14a2cc9b5ef src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Wed Aug 01 19:48:58 2018 +0200
+++ b/src/Doc/System/Sessions.thy	Wed Aug 01 20:58:41 2018 +0200
@@ -333,14 +333,14 @@
   completed by including all ancestors.
 
   \<^medskip>
-  One or more options \<^verbatim>\<open>-B\<close>~\<open>NAME\<close> specify base sessions. All descendants
-  are included.
+  One or more options \<^verbatim>\<open>-B\<close>~\<open>NAME\<close> specify base sessions to be included (all
+  descendants wrt.\ the session parent or import graph).
 
   \<^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
-  specified by session group membership.
+  One or more options \<^verbatim>\<open>-x\<close>~\<open>NAME\<close> specify sessions to be excluded (all
+  descendants wrt.\ the session parent or import graph). Option \<^verbatim>\<open>-X\<close> is
+  analogous to this, but excluded sessions are specified by session group
+  membership.
 
   \<^medskip>
   Option \<^verbatim>\<open>-R\<close> reverses the selection in the sense that it refers to its
@@ -373,8 +373,8 @@
   of sessions, as required for other sessions to continue later on.
 
   \<^medskip>
-  Option \<^verbatim>\<open>-c\<close> cleans all descendants of the selected sessions before
-  performing the specified build operation.
+  Option \<^verbatim>\<open>-c\<close> cleans the selected sessions (all descendants wrt.\ the session
+  parent or import graph) before performing the specified build operation.
 
   \<^medskip>
   Option \<^verbatim>\<open>-f\<close> forces a fresh build of all selected sessions and their
diff -r 76e339ef60e3 -r c14a2cc9b5ef src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Wed Aug 01 19:48:58 2018 +0200
+++ b/src/Pure/Thy/sessions.scala	Wed Aug 01 20:58:41 2018 +0200
@@ -668,7 +668,7 @@
       check_sessions(sel)
 
       val select_group = sel.session_groups.toSet
-      val select_session = sel.sessions.toSet ++ graph.all_succs(sel.base_sessions)
+      val select_session = sel.sessions.toSet ++ imports_graph.all_succs(sel.base_sessions)
 
       val selected0 =
         if (sel.all_sessions) graph.keys
@@ -693,10 +693,10 @@
         val exclude_group = sel.exclude_session_groups.toSet
         val exclude_group_sessions =
           (for {
-            (name, (info, _)) <- build_graph.iterator
-            if build_graph.get_node(name).groups.exists(exclude_group)
+            (name, (info, _)) <- imports_graph.iterator
+            if imports_graph.get_node(name).groups.exists(exclude_group)
           } yield name).toList
-        build_graph.all_succs(exclude_group_sessions ::: sel.exclude_sessions).toSet
+        imports_graph.all_succs(exclude_group_sessions ::: sel.exclude_sessions).toSet
       }
 
       def restrict(graph: Graph[String, Info]): Graph[String, Info] =
diff -r 76e339ef60e3 -r c14a2cc9b5ef src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Aug 01 19:48:58 2018 +0200
+++ b/src/Pure/Tools/build.scala	Wed Aug 01 20:58:41 2018 +0200
@@ -492,7 +492,7 @@
     store.prepare_output_dir()
 
     if (clean_build) {
-      for (name <- full_sessions.build_descendants(full_sessions.build_selection(selection1))) {
+      for (name <- full_sessions.imports_descendants(full_sessions.imports_selection(selection1))) {
         val (relevant, ok) = store.clean_output(name)
         if (relevant) {
           if (ok) progress.echo("Cleaned " + name)