# HG changeset patch # User noschinl # Date 1429265534 -7200 # Node ID 82f355352490cf13a92572fe7be7ebbde37132f8 # Parent 22389d4cdd6bc5e73ff1d941c69606fc588ee220# Parent aedbc0413d307212fe705a0acdc3e45afc697c6d merged diff -r 22389d4cdd6b -r 82f355352490 NEWS --- 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 diff -r 22389d4cdd6b -r 82f355352490 lib/Tools/build --- 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 diff -r 22389d4cdd6b -r 82f355352490 src/Doc/System/Sessions.thy --- 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 diff -r 22389d4cdd6b -r 82f355352490 src/Pure/Tools/build.scala --- 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 _) } } - diff -r 22389d4cdd6b -r 82f355352490 src/ZF/ROOT --- 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*) -