allow to exclude session groups;
authorwenzelm
Fri Apr 17 11:28:57 2015 +0200 (2015-04-17)
changeset 60106e0d1d9203275
parent 60105 8614f8f0fb4b
child 60107 aedbc0413d30
allow to exclude session groups;
NEWS
lib/Tools/build
src/Doc/System/Sessions.thy
src/Pure/Tools/build.scala
     1.1 --- a/NEWS	Fri Apr 17 09:56:12 2015 +0200
     1.2 +++ b/NEWS	Fri Apr 17 11:28:57 2015 +0200
     1.3 @@ -449,7 +449,7 @@
     1.4  * The Isabelle tool "update_cartouches" changes theory files to use
     1.5  cartouches instead of old-style {* verbatim *} or `alt_string` tokens.
     1.6  
     1.7 -* The Isabelle tool "build" provides new options -k and -x.
     1.8 +* The Isabelle tool "build" provides new options -X, -k, -x.
     1.9  
    1.10  * Discontinued old-fashioned "codegen" tool. Code generation can always
    1.11  be externally triggered using an appropriate ROOT file plus a
     2.1 --- a/lib/Tools/build	Fri Apr 17 09:56:12 2015 +0200
     2.2 +++ b/lib/Tools/build	Fri Apr 17 11:28:57 2015 +0200
     2.3 @@ -28,6 +28,7 @@
     2.4    echo "  Options are:"
     2.5    echo "    -D DIR       include session directory and select its sessions"
     2.6    echo "    -R           operate on requirements of selected sessions"
     2.7 +  echo "    -X NAME      exclude sessions from group NAME and all descendants"
     2.8    echo "    -a           select all sessions"
     2.9    echo "    -b           build heap images"
    2.10    echo "    -c           clean build"
    2.11 @@ -40,7 +41,7 @@
    2.12    echo "    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)"
    2.13    echo "    -s           system build mode: produce output in ISABELLE_HOME"
    2.14    echo "    -v           verbose"
    2.15 -  echo "    -x SESSION   exclude SESSION and all its descendants"
    2.16 +  echo "    -x NAME      exclude session NAME and all descendants"
    2.17    echo
    2.18    echo "  Build and manage Isabelle sessions, depending on implicit"
    2.19    show_settings "  "
    2.20 @@ -64,6 +65,7 @@
    2.21  
    2.22  declare -a SELECT_DIRS=()
    2.23  REQUIREMENTS=false
    2.24 +declare -a EXCLUDE_SESSION_GROUPS=()
    2.25  ALL_SESSIONS=false
    2.26  BUILD_HEAP=false
    2.27  CLEAN_BUILD=false
    2.28 @@ -78,7 +80,7 @@
    2.29  VERBOSE=false
    2.30  declare -a EXCLUDE_SESSIONS=()
    2.31  
    2.32 -while getopts "D:Rabcd:g:j:k:lno:svx:" OPT
    2.33 +while getopts "D:RX:abcd:g:j:k:lno:svx:" OPT
    2.34  do
    2.35    case "$OPT" in
    2.36      D)
    2.37 @@ -87,6 +89,9 @@
    2.38      R)
    2.39        REQUIREMENTS="true"
    2.40        ;;
    2.41 +    X)
    2.42 +      EXCLUDE_SESSION_GROUPS["${#EXCLUDE_SESSION_GROUPS[@]}"]="$OPTARG"
    2.43 +      ;;
    2.44      a)
    2.45        ALL_SESSIONS="true"
    2.46        ;;
    2.47 @@ -156,7 +161,8 @@
    2.48    "$LIST_FILES" "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \
    2.49    "${INCLUDE_DIRS[@]}" $'\n' "${SELECT_DIRS[@]}" $'\n' \
    2.50    "${SESSION_GROUPS[@]}" $'\n' "${CHECK_KEYWORDS[@]}" $'\n' \
    2.51 -  "${BUILD_OPTIONS[@]}" $'\n' "${EXCLUDE_SESSIONS[@]}" $'\n' "$@"
    2.52 +  "${BUILD_OPTIONS[@]}" $'\n' "${EXCLUDE_SESSION_GROUPS[@]}" $'\n' \
    2.53 +  "${EXCLUDE_SESSIONS[@]}" $'\n' "$@"
    2.54  RC="$?"
    2.55  
    2.56  if [ "$NO_BUILD" = false -a "$VERBOSE" = true ]; then
     3.1 --- a/src/Doc/System/Sessions.thy	Fri Apr 17 09:56:12 2015 +0200
     3.2 +++ b/src/Doc/System/Sessions.thy	Fri Apr 17 11:28:57 2015 +0200
     3.3 @@ -278,6 +278,7 @@
     3.4    Options are:
     3.5      -D DIR       include session directory and select its sessions
     3.6      -R           operate on requirements of selected sessions
     3.7 +    -X NAME      exclude sessions from group NAME and all descendants
     3.8      -a           select all sessions
     3.9      -b           build heap images
    3.10      -c           clean build
    3.11 @@ -290,7 +291,7 @@
    3.12      -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
    3.13      -s           system build mode: produce output in ISABELLE_HOME
    3.14      -v           verbose
    3.15 -    -x SESSION   exclude SESSION and all its descendants
    3.16 +    -x NAME      exclude session NAME and all descendants
    3.17  
    3.18    Build and manage Isabelle sessions, depending on implicit
    3.19    ISABELLE_BUILD_OPTIONS="..."
    3.20 @@ -323,9 +324,11 @@
    3.21    The build tool takes session dependencies into account: the set of
    3.22    selected sessions is completed by including all ancestors.
    3.23  
    3.24 -  \medskip One or more options @{verbatim "-x"}~@{text SESSION} specify
    3.25 +  \medskip One or more options @{verbatim "-x"}~@{text NAME} specify
    3.26    sessions to be excluded. All descendents of excluded sessions are removed
    3.27 -  from the selection as specified above.
    3.28 +  from the selection as specified above. Option @{verbatim "-X"} is
    3.29 +  analogous to this, but excluded sessions are specified by session group
    3.30 +  membership.
    3.31  
    3.32    \medskip Option @{verbatim "-R"} reverses the selection in the sense
    3.33    that it refers to its requirements: all ancestor sessions excluding
     4.1 --- a/src/Pure/Tools/build.scala	Fri Apr 17 09:56:12 2015 +0200
     4.2 +++ b/src/Pure/Tools/build.scala	Fri Apr 17 11:28:57 2015 +0200
     4.3 @@ -165,15 +165,26 @@
     4.4      def selection(
     4.5        requirements: Boolean = false,
     4.6        all_sessions: Boolean = false,
     4.7 +      exclude_session_groups: List[String] = Nil,
     4.8 +      exclude_sessions: List[String] = Nil,
     4.9        session_groups: List[String] = Nil,
    4.10 -      exclude_sessions: List[String] = Nil,
    4.11        sessions: List[String] = Nil): (List[String], Session_Tree) =
    4.12      {
    4.13        val bad_sessions =
    4.14          SortedSet((exclude_sessions ::: sessions).filterNot(isDefinedAt(_)): _*).toList
    4.15        if (bad_sessions.nonEmpty) error("Undefined session(s): " + commas_quote(bad_sessions))
    4.16  
    4.17 -      val excluded = graph.all_succs(exclude_sessions).toSet
    4.18 +      val excluded =
    4.19 +      {
    4.20 +        val exclude_group = exclude_session_groups.toSet
    4.21 +        val exclude_group_sessions =
    4.22 +          (for {
    4.23 +            (name, (info, _)) <- graph.iterator
    4.24 +            if apply(name).groups.exists(exclude_group)
    4.25 +          } yield name).toList
    4.26 +        graph.all_succs(exclude_group_sessions ::: exclude_sessions).toSet
    4.27 +      }
    4.28 +
    4.29        val pre_selected =
    4.30        {
    4.31          if (all_sessions) graph.keys
    4.32 @@ -751,6 +762,7 @@
    4.33      clean_build: Boolean = false,
    4.34      dirs: List[Path] = Nil,
    4.35      select_dirs: List[Path] = Nil,
    4.36 +    exclude_session_groups: List[String] = Nil,
    4.37      session_groups: List[String] = Nil,
    4.38      max_jobs: Int = 1,
    4.39      list_files: Boolean = false,
    4.40 @@ -765,7 +777,8 @@
    4.41  
    4.42      val full_tree = find_sessions(options.int("completion_limit") = 0, dirs, select_dirs)
    4.43      val (selected, selected_tree) =
    4.44 -      full_tree.selection(requirements, all_sessions, session_groups, exclude_sessions, sessions)
    4.45 +      full_tree.selection(requirements, all_sessions,
    4.46 +        exclude_session_groups, exclude_sessions, session_groups, sessions)
    4.47  
    4.48      val deps = dependencies(progress, true, verbose, list_files, check_keywords, selected_tree)
    4.49  
    4.50 @@ -1004,6 +1017,7 @@
    4.51      clean_build: Boolean = false,
    4.52      dirs: List[Path] = Nil,
    4.53      select_dirs: List[Path] = Nil,
    4.54 +    exclude_session_groups: List[String] = Nil,
    4.55      session_groups: List[String] = Nil,
    4.56      max_jobs: Int = 1,
    4.57      list_files: Boolean = false,
    4.58 @@ -1016,8 +1030,8 @@
    4.59    {
    4.60      val results =
    4.61        build_results(options, progress, requirements, all_sessions, build_heap, clean_build,
    4.62 -        dirs, select_dirs, session_groups, max_jobs, list_files, check_keywords,
    4.63 -        no_build, system_mode, verbose, exclude_sessions, sessions)
    4.64 +        dirs, select_dirs, exclude_session_groups, session_groups, max_jobs, list_files,
    4.65 +        check_keywords, no_build, system_mode, verbose, exclude_sessions, sessions)
    4.66  
    4.67      val rc = (0 /: results)({ case (rc1, (_, rc2)) => rc1 max rc2 })
    4.68      if (rc != 0 && (verbose || !no_build)) {
    4.69 @@ -1046,13 +1060,13 @@
    4.70            Properties.Value.Boolean(system_mode) ::
    4.71            Properties.Value.Boolean(verbose) ::
    4.72            Command_Line.Chunks(dirs, select_dirs, session_groups, check_keywords,
    4.73 -              build_options, exclude_sessions, sessions) =>
    4.74 +              build_options, exclude_session_groups, exclude_sessions, sessions) =>
    4.75              val options = (Options.init() /: build_options)(_ + _)
    4.76              val progress = new Console_Progress(verbose)
    4.77              progress.interrupt_handler {
    4.78                build(options, progress, requirements, all_sessions, build_heap, clean_build,
    4.79 -                dirs.map(Path.explode(_)), select_dirs.map(Path.explode(_)), session_groups,
    4.80 -                max_jobs, list_files, check_keywords.toSet, no_build, system_mode,
    4.81 +                dirs.map(Path.explode(_)), select_dirs.map(Path.explode(_)), exclude_session_groups,
    4.82 +                session_groups, max_jobs, list_files, check_keywords.toSet, no_build, system_mode,
    4.83                  verbose, exclude_sessions, sessions)
    4.84              }
    4.85          case _ => error("Bad arguments:\n" + cat_lines(args))
    4.86 @@ -1116,4 +1130,3 @@
    4.87          Markup.LOADING_THEORY -> loading_theory _)
    4.88    }
    4.89  }
    4.90 -