--- a/Admin/lib/Tools/build_doc Tue Sep 04 18:49:40 2012 +0200
+++ b/Admin/lib/Tools/build_doc Tue Sep 04 20:45:43 2012 +0200
@@ -17,7 +17,7 @@
echo " Options are:"
echo " -a select all doc sessions"
echo " -j INT maximum number of parallel jobs (default 1)"
- echo " -p approximative build of pdf documents"
+ echo " -p build only pdf documents"
echo
echo " Build Isabelle documentation from (doc) sessions."
echo
@@ -38,6 +38,8 @@
## process command line
+# options
+
ALL_DOCS="false"
JOBS=""
PDF_ONLY=""
@@ -63,32 +65,44 @@
shift $(($OPTIND - 1))
+
+# arguments
+
if [ "$ALL_DOCS" = true ]; then
- declare -a BUILD_OPTIONS=(-g doc)
+ declare -a BUILD_ARGS=(-g doc)
else
- declare -a BUILD_OPTIONS=()
+ declare -a BUILD_ARGS=()
[ "$#" -eq 0 ] && usage
fi
+BUILD_ARGS["${#BUILD_ARGS[@]}"]="--"
+
+while [ "$#" -ne 0 ]; do
+ BUILD_ARGS["${#BUILD_ARGS[@]}"]="$1"
+ shift
+done
+
## main
OUTPUT="$ISABELLE_TMP_PREFIX$$"
mkdir -p "$OUTPUT" || fail "Bad directory: \"$OUTPUT\""
+"$ISABELLE_TOOL" build -R -b $JOBS "${BUILD_ARGS[@]}"
+RC=$?
+
if [ "$PDF_ONLY" = true ]; then
FORMATS="pdf"
else
- FORMATS="false dvi pdf"
+ FORMATS="dvi pdf"
fi
-RC=0
for FORMAT in $FORMATS
do
if [ "$RC" = 0 ]; then
echo "Document format: $FORMAT"
"$ISABELLE_TOOL" build -o browser_info=false -o "document=$FORMAT" \
- -o "document_output=$OUTPUT" -c $JOBS "${BUILD_OPTIONS[@]}" -- "$@"
+ -o "document_output=$OUTPUT" -c $JOBS "${BUILD_ARGS[@]}"
RC=$?
fi
done
@@ -100,7 +114,6 @@
done
if [ "$PDF_ONLY" = true ]; then
cp -f "$OUTPUT"/*.pdf "$ISABELLE_HOME/doc"
- rm -f "$ISABELLE_HOME/doc/document.pdf" "$ISABELLE_HOME/doc/outline.pdf"
else
cp -f "$OUTPUT"/*.dvi "$OUTPUT"/*.pdf "$ISABELLE_HOME/doc"
fi
--- a/lib/Tools/build Tue Sep 04 18:49:40 2012 +0200
+++ b/lib/Tools/build Tue Sep 04 20:45:43 2012 +0200
@@ -27,6 +27,7 @@
echo
echo " Options are:"
echo " -D DIR include session directory and select its sessions"
+ echo " -R operate on requirements of selected sessions"
echo " -a select all sessions"
echo " -b build heap images"
echo " -c clean build"
@@ -60,6 +61,7 @@
## process command line
declare -a SELECT_DIRS=()
+REQUIREMENTS=false
ALL_SESSIONS=false
BUILD_HEAP=false
CLEAN_BUILD=false
@@ -72,12 +74,15 @@
SYSTEM_MODE=false
VERBOSE=false
-while getopts "D:abcd:g:j:lno:sv" OPT
+while getopts "D:Rabcd:g:j:lno:sv" OPT
do
case "$OPT" in
D)
SELECT_DIRS["${#SELECT_DIRS[@]}"]="$OPTARG"
;;
+ R)
+ REQUIREMENTS="true"
+ ;;
a)
ALL_SESSIONS="true"
;;
@@ -135,7 +140,7 @@
. "$ISABELLE_HOME/lib/scripts/timestart.bash"
"$ISABELLE_TOOL" java isabelle.Build \
- "$ALL_SESSIONS" "$BUILD_HEAP" "$CLEAN_BUILD" "$MAX_JOBS" \
+ "$REQUIREMENTS" "$ALL_SESSIONS" "$BUILD_HEAP" "$CLEAN_BUILD" "$MAX_JOBS" \
"$LIST_FILES" "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \
"${SELECT_DIRS[@]}" $'\n' "${INCLUDE_DIRS[@]}" $'\n' \
"${SESSION_GROUPS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"
--- a/src/Doc/System/Sessions.thy Tue Sep 04 18:49:40 2012 +0200
+++ b/src/Doc/System/Sessions.thy Tue Sep 04 20:45:43 2012 +0200
@@ -183,6 +183,7 @@
Options are:
-D DIR include session directory and select its sessions
+ -R operate on requirements of selected sessions
-a select all sessions
-b build heap images
-c clean build
@@ -227,6 +228,12 @@
The build tool takes session dependencies into account: the set of
selected sessions is completed by including all ancestors.
+ \medskip Option @{verbatim "-R"} reverses the selection in the sense
+ that it refers to its requirements: all ancestor sessions excluding
+ the original selection. This allows to prepare the stage for some
+ build process with different options, before running the main build
+ itself (without option @{verbatim "-R"}).
+
\medskip Option @{verbatim "-D"} is similar to @{verbatim "-d"}, but
selects all sessions that are defined in the given directories.
@@ -319,6 +326,12 @@
\begin{ttbox}
isabelle build -D '$AFP'
\end{ttbox}
+
+ \smallskip Inform about the status of all sessions required for AFP,
+ without building anything yet:
+\begin{ttbox}
+isabelle build -D '$AFP' -R -v -n
+\end{ttbox}
*}
end
--- a/src/Pure/System/build.scala Tue Sep 04 18:49:40 2012 +0200
+++ b/src/Pure/System/build.scala Tue Sep 04 20:45:43 2012 +0200
@@ -120,13 +120,13 @@
def apply(name: String): Session_Info = graph.get_node(name)
def isDefinedAt(name: String): Boolean = graph.defined(name)
- def required(all_sessions: Boolean, session_groups: List[String], sessions: List[String])
- : (List[String], Session_Tree) =
+ def selection(requirements: Boolean, all_sessions: Boolean,
+ session_groups: List[String], sessions: List[String]): (List[String], Session_Tree) =
{
val bad_sessions = sessions.filterNot(isDefinedAt(_))
if (!bad_sessions.isEmpty) error("Undefined session(s): " + commas_quote(bad_sessions))
- val selected =
+ val pre_selected =
{
if (all_sessions) graph.keys.toList
else {
@@ -138,9 +138,12 @@
} yield name).toList
}
}
- val descendants = graph.all_succs(selected)
+ val selected =
+ if (requirements) (graph.all_preds(pre_selected).toSet -- pre_selected).toList
+ else pre_selected
+
val tree1 = new Session_Tree(graph.restrict(graph.all_preds(selected).toSet))
- (descendants, tree1)
+ (selected, tree1)
}
def topological_order: List[(String, Session_Info)] =
@@ -384,8 +387,9 @@
def session_content(inlined_files: Boolean, dirs: List[Path], session: String): Session_Content =
{
+ val options = Options.init
val (_, tree) =
- find_sessions(Options.init(), dirs.map((false, _))).required(false, Nil, List(session))
+ find_sessions(options, dirs.map((false, _))).selection(false, false, Nil, List(session))
dependencies(inlined_files, false, false, tree)(session)
}
@@ -533,6 +537,7 @@
/* build */
def build(
+ requirements: Boolean = false,
all_sessions: Boolean = false,
build_heap: Boolean = false,
clean_build: Boolean = false,
@@ -547,13 +552,15 @@
sessions: List[String] = Nil): Int =
{
val options = (Options.init() /: build_options)(_ + _)
- val (descendants, tree) =
- find_sessions(options, more_dirs).required(all_sessions, session_groups, sessions)
- val deps = dependencies(true, verbose, list_files, tree)
- val queue = Queue(tree)
+ val full_tree = find_sessions(options, more_dirs)
+ val (selected, selected_tree) =
+ full_tree.selection(requirements, all_sessions, session_groups, sessions)
+
+ val deps = dependencies(true, verbose, list_files, selected_tree)
+ val queue = Queue(selected_tree)
def make_stamp(name: String): String =
- sources_stamp(tree(name).entry_digest :: deps.sources(name))
+ sources_stamp(selected_tree(name).entry_digest :: deps.sources(name))
val (input_dirs, output_dir, browser_info) =
if (system_mode) {
@@ -571,7 +578,7 @@
// optional cleanup
if (clean_build) {
- for (name <- descendants) {
+ for (name <- full_tree.graph.all_succs(selected)) {
val files =
List(Path.basic(name), log(name), log_gz(name)).map(output_dir + _).filter(_.is_file)
if (!files.isEmpty) echo("Cleaning " + name + " ...")
@@ -697,6 +704,7 @@
Command_Line.tool {
args.toList match {
case
+ Properties.Value.Boolean(requirements) ::
Properties.Value.Boolean(all_sessions) ::
Properties.Value.Boolean(build_heap) ::
Properties.Value.Boolean(clean_build) ::
@@ -709,7 +717,7 @@
val dirs =
select_dirs.map(d => (true, Path.explode(d))) :::
include_dirs.map(d => (false, Path.explode(d)))
- build(all_sessions, build_heap, clean_build, dirs, session_groups,
+ build(requirements, all_sessions, build_heap, clean_build, dirs, session_groups,
max_jobs, list_files, no_build, build_options, system_mode, verbose, sessions)
case _ => error("Bad arguments:\n" + cat_lines(args))
}