# HG changeset patch
# User wenzelm
# Date 1476954316 -7200
# Node ID 96fef7745c684216ed798f8438dc2e7b6e708dfb
# Parent  e48e2532ac171f5a885b461ae35b24f3c7910672
build HTML library in Isabelle/Scala;

diff -r e48e2532ac17 -r 96fef7745c68 Admin/Release/build_library
--- a/Admin/Release/build_library	Thu Oct 20 11:04:38 2016 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,93 +0,0 @@
-#!/usr/bin/env bash
-#
-# build Isabelle HTML library from platform bundle
-
-## diagnostics
-
-PRG=$(basename "$0")
-
-function usage()
-{
-  echo
-  echo "Usage: $PRG [OPTIONS] ARCHIVE"
-  echo
-  echo "  Options are:"
-  echo "    -j INT       maximum number of parallel jobs (default 1)"
-  echo
-  echo "  Build Isabelle HTML library from platform bundle."
-  echo
-  exit 1
-}
-
-function fail()
-{
-  echo "$1" >&2
-  exit 2
-}
-
-
-## process command line
-
-# options
-
-JOBS=""
-
-while getopts "j:" OPT
-do
-  case "$OPT" in
-    j)
-      JOBS="-j $OPTARG"
-      ;;
-    \?)
-      usage
-      ;;
-  esac
-done
-
-shift $(($OPTIND - 1))
-
-
-# args
-
-[ "$#" -ne 1 ] && usage
-
-ARCHIVE="$1"; shift
-
-[ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE"
-ARCHIVE_BASE="$(basename "$ARCHIVE")"
-ARCHIVE_DIR="$(cd "$(dirname "$ARCHIVE")"; echo "$PWD")"
-ARCHIVE_FULL="$ARCHIVE_DIR/$ARCHIVE_BASE"
-
-
-## main
-
-#GNU tar (notably on Mac OS X)
-type -p gnutar >/dev/null && function tar() { gnutar "$@"; }
-
-TMP="/var/tmp/isabelle-makedist$$"
-mkdir "$TMP" || fail "Cannot create directory: \"$TMP\""
-
-cd "$TMP"
-tar -x -z -f "$ARCHIVE_FULL"
-
-cd *
-ISABELLE_NAME="$(basename "$PWD")"
-
-env ISABELLE_IDENTIFIER="${ISABELLE_NAME}-build" \
-  ./bin/isabelle build $JOBS -s -c -a -d '~~/src/Benchmarks' -o browser_info \
-    -o "document=pdf" -o "document_variants=document:outline=/proof,/ML"
-RC="$?"
-
-cd ..
-
-if [ "$RC" = 0 ]; then
-  chmod -R a+r "$ISABELLE_NAME"
-  chmod -R g=o "$ISABELLE_NAME"
-  tar -c -z -f "$ARCHIVE_DIR/${ISABELLE_NAME}_library.tar.gz" "$ISABELLE_NAME/browser_info"
-fi
-
-# clean up
-cd /tmp
-rm -rf "$TMP"
-
-exit "$RC"
diff -r e48e2532ac17 -r 96fef7745c68 src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Thu Oct 20 11:04:38 2016 +0200
+++ b/src/Pure/Admin/build_release.scala	Thu Oct 20 11:05:16 2016 +0200
@@ -150,10 +150,29 @@
         progress.echo("### Library archive already exists: " +
           release_info.dist_library_archive.implode)
       else {
-        progress.bash("\"$ISABELLE_HOME/Admin/Release/build_library\"" + jobs_option + " " +
-          File.bash_path(release_info.dist_dir +
-            Path.explode(release_info.name + "_" +
-              Isabelle_System.getenv_strict("ISABELLE_PLATFORM_FAMILY") + ".tar.gz"))).check
+        Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
+          {
+            def execute(script: String): Unit =
+              Isabelle_System.bash(script, cwd = tmp_dir.file).check
+
+            val name = release_info.name
+            val platform = Isabelle_System.getenv_strict("ISABELLE_PLATFORM_FAMILY")
+            val bundle = release_info.dist_dir + Path.explode(name + "_" + platform + ".tar.gz")
+            execute("tar xzf " + File.bash_path(bundle))
+
+            val other_isabelle =
+              new Other_Isabelle(progress, tmp_dir + Path.explode(name), name + "-build")
+
+            other_isabelle.bash("bin/isabelle build" + jobs_option +
+                " -o browser_info -o document=pdf -o document_variants=document:outline=/proof,/ML" +
+                " -s -c -a -d '~~/src/Benchmarks'", echo = true).check
+            other_isabelle.isabelle_home_user.file.delete
+
+            execute("chmod -R a+r " + Bash.string(name))
+            execute("chmod -R g=o " + Bash.string(name))
+            execute("tar czf " + File.bash_path(release_info.dist_library_archive) +
+              " " + Bash.string(name + "/browser_info"))
+          })
       }
     }
 
@@ -198,7 +217,7 @@
         "R:" -> (arg => release_name = arg),
         "W:" -> (arg => website = Some(Path.explode(arg))),
         "j:" -> (arg => parallel_jobs = Value.Int.parse(arg)),
-        "l" -> (_ => build_library),
+        "l" -> (_ => build_library = true),
         "p:" -> (arg => platform_families = Library.space_explode(',', arg)),
         "r:" -> (arg => rev = arg))