isabelle build options -c -x -B refer to imports_graph;
authorwenzelm
Wed Aug 01 20:58:41 2018 +0200 (15 months ago ago)
changeset 68734c14a2cc9b5ef
parent 68733 76e339ef60e3
child 68735 2862b585a0db
isabelle build options -c -x -B refer to imports_graph;
NEWS
src/Doc/System/Sessions.thy
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.scala
     1.1 --- a/NEWS	Wed Aug 01 19:48:58 2018 +0200
     1.2 +++ b/NEWS	Wed Aug 01 20:58:41 2018 +0200
     1.3 @@ -473,6 +473,11 @@
     1.4    - option -S: only observe changes of sources, not heap images
     1.5    - option -f: forces a fresh build
     1.6  
     1.7 +* Command-line tool "isabelle build" options -c -x -B refer to
     1.8 +descendants wrt. the session parent or import graph. Subtle
     1.9 +INCOMPATIBILITY: options -c -x used to refer to the session parent graph
    1.10 +only.
    1.11 +
    1.12  * Command-line tool "isabelle build" takes "condition" options with the
    1.13  corresponding environment values into account, when determining the
    1.14  up-to-date status of a session.
     2.1 --- a/src/Doc/System/Sessions.thy	Wed Aug 01 19:48:58 2018 +0200
     2.2 +++ b/src/Doc/System/Sessions.thy	Wed Aug 01 20:58:41 2018 +0200
     2.3 @@ -333,14 +333,14 @@
     2.4    completed by including all ancestors.
     2.5  
     2.6    \<^medskip>
     2.7 -  One or more options \<^verbatim>\<open>-B\<close>~\<open>NAME\<close> specify base sessions. All descendants
     2.8 -  are included.
     2.9 +  One or more options \<^verbatim>\<open>-B\<close>~\<open>NAME\<close> specify base sessions to be included (all
    2.10 +  descendants wrt.\ the session parent or import graph).
    2.11  
    2.12    \<^medskip>
    2.13 -  One or more options \<^verbatim>\<open>-x\<close>~\<open>NAME\<close> specify sessions to be excluded. All
    2.14 -  descendents of excluded sessions are removed from the selection as specified
    2.15 -  above. Option \<^verbatim>\<open>-X\<close> is analogous to this, but excluded sessions are
    2.16 -  specified by session group membership.
    2.17 +  One or more options \<^verbatim>\<open>-x\<close>~\<open>NAME\<close> specify sessions to be excluded (all
    2.18 +  descendants wrt.\ the session parent or import graph). Option \<^verbatim>\<open>-X\<close> is
    2.19 +  analogous to this, but excluded sessions are specified by session group
    2.20 +  membership.
    2.21  
    2.22    \<^medskip>
    2.23    Option \<^verbatim>\<open>-R\<close> reverses the selection in the sense that it refers to its
    2.24 @@ -373,8 +373,8 @@
    2.25    of sessions, as required for other sessions to continue later on.
    2.26  
    2.27    \<^medskip>
    2.28 -  Option \<^verbatim>\<open>-c\<close> cleans all descendants of the selected sessions before
    2.29 -  performing the specified build operation.
    2.30 +  Option \<^verbatim>\<open>-c\<close> cleans the selected sessions (all descendants wrt.\ the session
    2.31 +  parent or import graph) before performing the specified build operation.
    2.32  
    2.33    \<^medskip>
    2.34    Option \<^verbatim>\<open>-f\<close> forces a fresh build of all selected sessions and their
     3.1 --- a/src/Pure/Thy/sessions.scala	Wed Aug 01 19:48:58 2018 +0200
     3.2 +++ b/src/Pure/Thy/sessions.scala	Wed Aug 01 20:58:41 2018 +0200
     3.3 @@ -668,7 +668,7 @@
     3.4        check_sessions(sel)
     3.5  
     3.6        val select_group = sel.session_groups.toSet
     3.7 -      val select_session = sel.sessions.toSet ++ graph.all_succs(sel.base_sessions)
     3.8 +      val select_session = sel.sessions.toSet ++ imports_graph.all_succs(sel.base_sessions)
     3.9  
    3.10        val selected0 =
    3.11          if (sel.all_sessions) graph.keys
    3.12 @@ -693,10 +693,10 @@
    3.13          val exclude_group = sel.exclude_session_groups.toSet
    3.14          val exclude_group_sessions =
    3.15            (for {
    3.16 -            (name, (info, _)) <- build_graph.iterator
    3.17 -            if build_graph.get_node(name).groups.exists(exclude_group)
    3.18 +            (name, (info, _)) <- imports_graph.iterator
    3.19 +            if imports_graph.get_node(name).groups.exists(exclude_group)
    3.20            } yield name).toList
    3.21 -        build_graph.all_succs(exclude_group_sessions ::: sel.exclude_sessions).toSet
    3.22 +        imports_graph.all_succs(exclude_group_sessions ::: sel.exclude_sessions).toSet
    3.23        }
    3.24  
    3.25        def restrict(graph: Graph[String, Info]): Graph[String, Info] =
     4.1 --- a/src/Pure/Tools/build.scala	Wed Aug 01 19:48:58 2018 +0200
     4.2 +++ b/src/Pure/Tools/build.scala	Wed Aug 01 20:58:41 2018 +0200
     4.3 @@ -492,7 +492,7 @@
     4.4      store.prepare_output_dir()
     4.5  
     4.6      if (clean_build) {
     4.7 -      for (name <- full_sessions.build_descendants(full_sessions.build_selection(selection1))) {
     4.8 +      for (name <- full_sessions.imports_descendants(full_sessions.imports_selection(selection1))) {
     4.9          val (relevant, ok) = store.clean_output(name)
    4.10          if (relevant) {
    4.11            if (ok) progress.echo("Cleaned " + name)