re-implemented build_doc in Isabelle/Scala;
clarified command-line: specify documentation files (via document_variants) instead of sessions;

--- a/Admin/lib/Tools/build_doc	Sat Apr 05 22:37:17 2014 +0200
+++ b/Admin/lib/Tools/build_doc	Sat Apr 05 23:17:30 2014 +0200
@@ -12,14 +12,15 @@
 function usage()
 {
   echo
-  echo "Usage: isabelle $PRG [OPTIONS] [SESSIONS ...]"
+  echo "Usage: isabelle $PRG [OPTIONS] [DOCS ...]"
   echo
   echo "  Options are:"
   echo "    -a           select all doc sessions"
   echo "    -j INT       maximum number of parallel jobs (default 1)"
   echo "    -s           system build mode"
   echo
-  echo "  Build Isabelle documentation from (doc) sessions."
+  echo "  Build Isabelle documentation from doc sessions with suitable"
+  echo "  document_variants."
   echo
   exit 1
 }
@@ -38,12 +39,9 @@
 
 ## process command line
 
-declare -a BUILD_ARGS=()
-
-
-# options
-
 ALL_DOCS="false"
+MAX_JOBS="1"
+SYSTEM_MODE="false"
 
 while getopts "aj:s" OPT
 do
@@ -53,11 +51,10 @@
       ;;
     j)
       check_number "$OPTARG"
-      BUILD_ARGS["${#BUILD_ARGS[@]}"]="-j"
-      BUILD_ARGS["${#BUILD_ARGS[@]}"]="$OPTARG"
+      MAX_JOBS="$OPTARG"
       ;;
     s)
-      BUILD_ARGS["${#BUILD_ARGS[@]}"]="-s"
+      SYSTEM_MODE="true"
       ;;
     \?)
       usage
@@ -67,42 +64,15 @@
 
 shift $(($OPTIND - 1))
 
-
-# arguments
-
-if [ "$ALL_DOCS" = true ]; then
-  BUILD_ARGS["${#BUILD_ARGS[@]}"]="-g"
-  BUILD_ARGS["${#BUILD_ARGS[@]}"]="doc"
-else
-  [ "$#" -eq 0 ] && usage
-fi
-
-BUILD_ARGS["${#BUILD_ARGS[@]}"]="--"
-
-while [ "$#" -ne 0 ]; do
-  BUILD_ARGS["${#BUILD_ARGS[@]}"]="$1"
-  shift
-done
+[ "$ALL_DOCS" = false -a "$#" -eq 0 ] && usage
 
 
 ## main
 
-OUTPUT="$ISABELLE_TMP_PREFIX$$"
-mkdir -p "$OUTPUT" || fail "Bad directory: \"$OUTPUT\""
+isabelle_admin_build jars || exit $?
 
-"$ISABELLE_TOOL" build -R -b "${BUILD_ARGS[@]}"
-RC=$?
+declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"
 
-if [ "$RC" = 0 ]; then
-  "$ISABELLE_TOOL" build -o browser_info=false -o "document=pdf" \
-    -o "document_output=$OUTPUT" -c "${BUILD_ARGS[@]}"
-  RC=$?
-fi
+"$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Build_Doc \
+  "$ALL_DOCS" "$MAX_JOBS" "$SYSTEM_MODE" "$@"
 
-if [ "$RC" = 0 ]; then
-  cp -f "$OUTPUT"/*.pdf "$ISABELLE_HOME/doc"
-fi
-
-rm -rf "$OUTPUT"
-
-exit $RC

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/build_doc.scala	Sat Apr 05 23:17:30 2014 +0200
@@ -0,0 +1,90 @@
+/*  Title:      Pure/Tools/build_doc.scala
+    Author:     Makarius
+
+Build Isabelle documentation.
+*/
+
+package isabelle
+
+
+import java.io.{File => JFile}
+
+
+object Build_Doc
+{
+  /* build_doc */
+
+  def build_doc(
+    options: Options,
+    progress: Build.Progress = Build.Ignore_Progress,
+    all_docs: Boolean = false,
+    max_jobs: Int = 1,
+    system_mode: Boolean = false,
+    docs: List[String] = Nil): Int =
+  {
+    val selection =
+      for {
+        (name, info) <- Build.find_sessions(options, Nil).topological_order
+        if info.groups.contains("doc")
+        doc = info.options.string("document_variants")
+        if all_docs || docs.contains(doc)
+      } yield (doc, name)
+
+    val selected_docs = selection.map(_._1)
+    val sessions = selection.map(_._2)
+
+    docs.filter(doc => !selected_docs.contains(doc)) match {
+      case Nil =>
+      case bad => error("No doc session for " + commas_quote(bad))
+    }
+
+
+    progress.echo("Build started for documentation " + commas_quote(selected_docs))
+    val rc1 =
+      Build.build(options, progress, requirements = true, build_heap = true,
+        max_jobs = max_jobs, system_mode = system_mode, sessions = sessions)
+    if (rc1 == 0) {
+      Isabelle_System.with_tmp_dir("document_output")(output =>
+        {
+          val rc2 =
+            Build.build(
+              options.bool.update("browser_info", false).
+                string.update("document", "pdf").
+                string.update("document_output", Isabelle_System.posix_path(output)),
+              progress, clean_build = true, sessions = sessions)
+          if (rc2 == 0) {
+            val doc_dir = Path.explode("$ISABELLE_HOME/doc").file
+            for (doc <- selected_docs) {
+              val name = doc + ".pdf"
+              File.copy(new JFile(output, name), new JFile(doc_dir, name))
+            }
+          }
+          rc2
+        })
+    }
+    else rc1
+  }
+
+
+  /* command line entry point */
+
+  def main(args: Array[String])
+  {
+    Command_Line.tool {
+      args.toList match {
+        case
+          Properties.Value.Boolean(all_docs) ::
+          Properties.Value.Int(max_jobs) ::
+          Properties.Value.Boolean(system_mode) ::
+          Command_Line.Chunks(docs) =>
+            val options = Options.init()
+            val progress = new Build.Console_Progress(false)
+            progress.interrupt_handler {
+              build_doc(options, progress, all_docs, max_jobs, system_mode, docs)
+            }
+        case _ => error("Bad arguments:\n" + cat_lines(args))
+      }
+    }
+  }
+}
+

--- a/src/Pure/build-jars	Sat Apr 05 22:37:17 2014 +0200
+++ b/src/Pure/build-jars	Sat Apr 05 23:17:30 2014 +0200
@@ -77,6 +77,7 @@
   Thy/thy_info.scala
   Thy/thy_syntax.scala
   Tools/build.scala
+  Tools/build_doc.scala
   Tools/doc.scala
   Tools/keywords.scala
   Tools/main.scala