# HG changeset patch
# User wenzelm
# Date 1346784343 -7200
# Node ID aa1e2ba3c697b81286df018ef0ec334a78416e04
# Parent  3c26e17b2849d46d67927bfb92ad170ef70c5b9b
added build option -R;
more precise build_doc, using build -R -b;

diff -r 3c26e17b2849 -r aa1e2ba3c697 Admin/lib/Tools/build_doc
--- 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
diff -r 3c26e17b2849 -r aa1e2ba3c697 lib/Tools/build
--- 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' "$@"
diff -r 3c26e17b2849 -r aa1e2ba3c697 src/Doc/System/Sessions.thy
--- 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
diff -r 3c26e17b2849 -r aa1e2ba3c697 src/Pure/System/build.scala
--- 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))
       }