--- 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.
--- 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
--- 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] =
--- 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)