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