--- a/NEWS Fri Apr 17 11:12:19 2015 +0200
+++ b/NEWS Fri Apr 17 12:12:14 2015 +0200
@@ -449,7 +449,7 @@
* The Isabelle tool "update_cartouches" changes theory files to use
cartouches instead of old-style {* verbatim *} or `alt_string` tokens.
-* The Isabelle tool "build" provides new options -k and -x.
+* The Isabelle tool "build" provides new options -X, -k, -x.
* Discontinued old-fashioned "codegen" tool. Code generation can always
be externally triggered using an appropriate ROOT file plus a
--- a/lib/Tools/build Fri Apr 17 11:12:19 2015 +0200
+++ b/lib/Tools/build Fri Apr 17 12:12:14 2015 +0200
@@ -28,6 +28,7 @@
echo " Options are:"
echo " -D DIR include session directory and select its sessions"
echo " -R operate on requirements of selected sessions"
+ echo " -X NAME exclude sessions from group NAME and all descendants"
echo " -a select all sessions"
echo " -b build heap images"
echo " -c clean build"
@@ -40,7 +41,7 @@
echo " -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)"
echo " -s system build mode: produce output in ISABELLE_HOME"
echo " -v verbose"
- echo " -x SESSION exclude SESSION and all its descendants"
+ echo " -x NAME exclude session NAME and all descendants"
echo
echo " Build and manage Isabelle sessions, depending on implicit"
show_settings " "
@@ -64,6 +65,7 @@
declare -a SELECT_DIRS=()
REQUIREMENTS=false
+declare -a EXCLUDE_SESSION_GROUPS=()
ALL_SESSIONS=false
BUILD_HEAP=false
CLEAN_BUILD=false
@@ -78,7 +80,7 @@
VERBOSE=false
declare -a EXCLUDE_SESSIONS=()
-while getopts "D:Rabcd:g:j:k:lno:svx:" OPT
+while getopts "D:RX:abcd:g:j:k:lno:svx:" OPT
do
case "$OPT" in
D)
@@ -87,6 +89,9 @@
R)
REQUIREMENTS="true"
;;
+ X)
+ EXCLUDE_SESSION_GROUPS["${#EXCLUDE_SESSION_GROUPS[@]}"]="$OPTARG"
+ ;;
a)
ALL_SESSIONS="true"
;;
@@ -156,7 +161,8 @@
"$LIST_FILES" "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \
"${INCLUDE_DIRS[@]}" $'\n' "${SELECT_DIRS[@]}" $'\n' \
"${SESSION_GROUPS[@]}" $'\n' "${CHECK_KEYWORDS[@]}" $'\n' \
- "${BUILD_OPTIONS[@]}" $'\n' "${EXCLUDE_SESSIONS[@]}" $'\n' "$@"
+ "${BUILD_OPTIONS[@]}" $'\n' "${EXCLUDE_SESSION_GROUPS[@]}" $'\n' \
+ "${EXCLUDE_SESSIONS[@]}" $'\n' "$@"
RC="$?"
if [ "$NO_BUILD" = false -a "$VERBOSE" = true ]; then
--- a/src/Doc/System/Sessions.thy Fri Apr 17 11:12:19 2015 +0200
+++ b/src/Doc/System/Sessions.thy Fri Apr 17 12:12:14 2015 +0200
@@ -278,6 +278,7 @@
Options are:
-D DIR include session directory and select its sessions
-R operate on requirements of selected sessions
+ -X NAME exclude sessions from group NAME and all descendants
-a select all sessions
-b build heap images
-c clean build
@@ -290,7 +291,7 @@
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-s system build mode: produce output in ISABELLE_HOME
-v verbose
- -x SESSION exclude SESSION and all its descendants
+ -x NAME exclude session NAME and all descendants
Build and manage Isabelle sessions, depending on implicit
ISABELLE_BUILD_OPTIONS="..."
@@ -323,9 +324,11 @@
The build tool takes session dependencies into account: the set of
selected sessions is completed by including all ancestors.
- \medskip One or more options @{verbatim "-x"}~@{text SESSION} specify
+ \medskip One or more options @{verbatim "-x"}~@{text NAME} specify
sessions to be excluded. All descendents of excluded sessions are removed
- from the selection as specified above.
+ from the selection as specified above. Option @{verbatim "-X"} is
+ analogous to this, but excluded sessions are specified by session group
+ membership.
\medskip Option @{verbatim "-R"} reverses the selection in the sense
that it refers to its requirements: all ancestor sessions excluding
--- a/src/Pure/Tools/build.scala Fri Apr 17 11:12:19 2015 +0200
+++ b/src/Pure/Tools/build.scala Fri Apr 17 12:12:14 2015 +0200
@@ -165,15 +165,26 @@
def selection(
requirements: Boolean = false,
all_sessions: Boolean = false,
+ exclude_session_groups: List[String] = Nil,
+ exclude_sessions: List[String] = Nil,
session_groups: List[String] = Nil,
- exclude_sessions: List[String] = Nil,
sessions: List[String] = Nil): (List[String], Session_Tree) =
{
val bad_sessions =
SortedSet((exclude_sessions ::: sessions).filterNot(isDefinedAt(_)): _*).toList
if (bad_sessions.nonEmpty) error("Undefined session(s): " + commas_quote(bad_sessions))
- val excluded = graph.all_succs(exclude_sessions).toSet
+ val excluded =
+ {
+ val exclude_group = exclude_session_groups.toSet
+ val exclude_group_sessions =
+ (for {
+ (name, (info, _)) <- graph.iterator
+ if apply(name).groups.exists(exclude_group)
+ } yield name).toList
+ graph.all_succs(exclude_group_sessions ::: exclude_sessions).toSet
+ }
+
val pre_selected =
{
if (all_sessions) graph.keys
@@ -751,6 +762,7 @@
clean_build: Boolean = false,
dirs: List[Path] = Nil,
select_dirs: List[Path] = Nil,
+ exclude_session_groups: List[String] = Nil,
session_groups: List[String] = Nil,
max_jobs: Int = 1,
list_files: Boolean = false,
@@ -765,7 +777,8 @@
val full_tree = find_sessions(options.int("completion_limit") = 0, dirs, select_dirs)
val (selected, selected_tree) =
- full_tree.selection(requirements, all_sessions, session_groups, exclude_sessions, sessions)
+ full_tree.selection(requirements, all_sessions,
+ exclude_session_groups, exclude_sessions, session_groups, sessions)
val deps = dependencies(progress, true, verbose, list_files, check_keywords, selected_tree)
@@ -1004,6 +1017,7 @@
clean_build: Boolean = false,
dirs: List[Path] = Nil,
select_dirs: List[Path] = Nil,
+ exclude_session_groups: List[String] = Nil,
session_groups: List[String] = Nil,
max_jobs: Int = 1,
list_files: Boolean = false,
@@ -1016,8 +1030,8 @@
{
val results =
build_results(options, progress, requirements, all_sessions, build_heap, clean_build,
- dirs, select_dirs, session_groups, max_jobs, list_files, check_keywords,
- no_build, system_mode, verbose, exclude_sessions, sessions)
+ dirs, select_dirs, exclude_session_groups, session_groups, max_jobs, list_files,
+ check_keywords, no_build, system_mode, verbose, exclude_sessions, sessions)
val rc = (0 /: results)({ case (rc1, (_, rc2)) => rc1 max rc2 })
if (rc != 0 && (verbose || !no_build)) {
@@ -1046,13 +1060,13 @@
Properties.Value.Boolean(system_mode) ::
Properties.Value.Boolean(verbose) ::
Command_Line.Chunks(dirs, select_dirs, session_groups, check_keywords,
- build_options, exclude_sessions, sessions) =>
+ build_options, exclude_session_groups, exclude_sessions, sessions) =>
val options = (Options.init() /: build_options)(_ + _)
val progress = new Console_Progress(verbose)
progress.interrupt_handler {
build(options, progress, requirements, all_sessions, build_heap, clean_build,
- dirs.map(Path.explode(_)), select_dirs.map(Path.explode(_)), session_groups,
- max_jobs, list_files, check_keywords.toSet, no_build, system_mode,
+ dirs.map(Path.explode(_)), select_dirs.map(Path.explode(_)), exclude_session_groups,
+ session_groups, max_jobs, list_files, check_keywords.toSet, no_build, system_mode,
verbose, exclude_sessions, sessions)
}
case _ => error("Bad arguments:\n" + cat_lines(args))
@@ -1116,4 +1130,3 @@
Markup.LOADING_THEORY -> loading_theory _)
}
}
-
--- a/src/ZF/ROOT Fri Apr 17 11:12:19 2015 +0200
+++ b/src/ZF/ROOT Fri Apr 17 12:12:14 2015 +0200
@@ -1,6 +1,6 @@
chapter ZF
-session ZF (main) = Pure +
+session ZF (main ZF) = Pure +
description {*
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1995 University of Cambridge
@@ -47,7 +47,7 @@
Main_ZFC
document_files "root.tex"
-session "ZF-AC" in AC = ZF +
+session "ZF-AC" (ZF) in AC = ZF +
description {*
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1995 University of Cambridge
@@ -75,7 +75,7 @@
DC
document_files "root.tex" "root.bib"
-session "ZF-Coind" in Coind = ZF +
+session "ZF-Coind" (ZF) in Coind = ZF +
description {*
Author: Jacob Frost, Cambridge University Computer Laboratory
Copyright 1995 University of Cambridge
@@ -101,7 +101,7 @@
options [document = false]
theories ECR
-session "ZF-Constructible" in Constructible = ZF +
+session "ZF-Constructible" (ZF) in Constructible = ZF +
description {*
Relative Consistency of the Axiom of Choice:
Inner Models, Absoluteness and Consistency Proofs.
@@ -127,7 +127,7 @@
Rank_Separation
document_files "root.tex" "root.bib"
-session "ZF-IMP" in IMP = ZF +
+session "ZF-IMP" (ZF) in IMP = ZF +
description {*
Author: Heiko Loetzbeyer & Robert Sandner, TUM
Copyright 1994 TUM
@@ -145,7 +145,7 @@
theories Equiv
document_files "root.tex" "root.bib"
-session "ZF-Induct" in Induct = ZF +
+session "ZF-Induct" (ZF) in Induct = ZF +
description {*
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 2001 University of Cambridge
@@ -178,7 +178,7 @@
"root.bib"
"root.tex"
-session "ZF-Resid" in Resid = ZF +
+session "ZF-Resid" (ZF) in Resid = ZF +
description {*
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1995 University of Cambridge
@@ -198,7 +198,7 @@
options [document = false]
theories Confluence
-session "ZF-UNITY" in UNITY = ZF +
+session "ZF-UNITY" (ZF) in UNITY = ZF +
description {*
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
@@ -216,7 +216,7 @@
(*Prefix relation; the Allocator example*)
Distributor Merge ClientImpl AllocImpl
-session "ZF-ex" in ex = ZF +
+session "ZF-ex" (ZF) in ex = ZF +
description {*
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
@@ -243,4 +243,3 @@
Limit (*Inverse limit construction of domains*)
BinEx (*Binary integer arithmetic*)
LList CoUnit (*CoDatatypes*)
-