# HG changeset patch
# User wenzelm
# Date 1346268046 -7200
# Node ID 3a324a3f4aea864b346295e9567b8ca1c1c358cc
# Parent  09a9761cf5ae1fea79e491646e0573ada94ad9c4
more formal isabelle makedist from repository;

diff -r 09a9761cf5ae -r 3a324a3f4aea Admin/Release/CHECKLIST
--- a/Admin/Release/CHECKLIST	Wed Aug 29 21:01:05 2012 +0200
+++ b/Admin/Release/CHECKLIST	Wed Aug 29 21:20:46 2012 +0200
@@ -46,7 +46,7 @@
 Packaging
 =========
 
-- makedist -j jedit_build-XXXX -r DISTNAME
+- hg up -r DISTNAME && isabelle makedist -r DISTNAME;
 
 - makebin (multiplatform);
 
diff -r 09a9761cf5ae -r 3a324a3f4aea Admin/Release/makedist
--- a/Admin/Release/makedist	Wed Aug 29 21:01:05 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,233 +0,0 @@
-#!/usr/bin/env bash
-#
-# makedist -- make Isabelle source distribution
-
-## global settings
-
-REPOS_NAME="isabelle"
-REPOS="${REPOS:-http://isabelle.in.tum.de/repos/${REPOS_NAME}}"
-DISTPREFIX="${DISTPREFIX:-$HOME/tmp/isadist}"
-
-umask 022
-
-
-## diagnostics
-
-PRG="$(basename "$0")"
-THIS="$(cd $(dirname "$0"); pwd)"
-
-function usage()
-{
-  cat <<EOF
-
-Usage: $PRG [OPTIONS] [VERSION]
-
-  Options are:
-    -j JEDIT_BUILD     build Isabelle/jEdit via given jedit_build component
-    -r RELEASE         proper release with name"
-
-  Make Isabelle distribution from the main Mercurial repository at TUM.
-
-  VERSION identifies the snapshot, using usual Mercurial terminology;
-  the default is RELEASE if given, otherwise "tip".
-
-EOF
-  exit 1
-}
-
-function fail()
-{
-  echo "$1" >&2
-  exit 2
-}
-
-
-## process command line
-
-# options
-
-RELEASE=""
-ISABELLE_JEDIT_BUILD_HOME=""
-
-while getopts "j:r:" OPT
-do
-  case "$OPT" in
-    j)
-      ISABELLE_JEDIT_BUILD_HOME="$OPTARG"
-      ;;
-    r)
-      RELEASE="$OPTARG"
-      ;;
-    \?)
-      usage
-      ;;
-  esac
-done
-
-shift $(($OPTIND - 1))
-
-
-# args
-
-VERSION=""
-[ "$#" -gt 0 ] && { VERSION="$1"; shift; }
-[ -z "$VERSION" ] && VERSION="$RELEASE"
-[ -z "$VERSION" ] && VERSION="tip"
-
-[ "$#" -gt 0 ] && usage
-
-
-## main
-
-# tmp
-
-TMP="tmp-$USER$$"
-function purge_tmp () { rm -rf "$DISTPREFIX/$TMP"; }
-
-
-# retrieve archive and resolve version identifier
-
-mkdir "$DISTPREFIX/$TMP" || fail "Failed to create fresh directory"
-cd "$DISTPREFIX/$TMP"
-
-echo "###"
-echo "### Retrieving Mercurial repository $VERSION"
-echo "###"
-
-if expr match "$REPOS" "https\?://" > /dev/null
-then
-  { wget -q "$REPOS/archive/${VERSION}.tar.gz" -O- | tar -xzf -; } || \
-    fail "Failed to retrieve $VERSION"
-else
-  { hg --repository "$REPOS" archive --type tgz - | tar -xzf -; } || \
-    fail "Failed to retrieve $VERSION"
-fi
-
-IDENT=$(echo * | sed "s/${REPOS_NAME}-//")
-
-rm -f "${REPOS_NAME}-${IDENT}/.hg_archival.txt"
-rm -f "${REPOS_NAME}-${IDENT}/.hgtags"
-rm -f "${REPOS_NAME}-${IDENT}/.hgignore"
-rm -f "${REPOS_NAME}-${IDENT}/README_REPOSITORY"
-
-
-# dist name
-
-DATE=$(env LC_ALL=C date "+%d-%b-%Y")
-DISTDATE=$(env LC_ALL=C date "+%B %Y")
-
-if [ -z "$RELEASE" ]; then
-  DISTNAME="Isabelle_$DATE"
-  DISTVERSION="Isabelle repository snapshot $IDENT $DATE"
-else
-  DISTNAME="$RELEASE"
-  DISTVERSION="$DISTNAME: $DISTDATE"
-fi
-
-DISTBASE="$DISTPREFIX/dist-$DISTNAME"
-mkdir -p "$DISTBASE" || { purge_tmp; fail "Unable to create distribution base dir $DISTBASE!"; }
-[ -e "$DISTBASE/$DISTNAME" ] && { purge_tmp; fail "$DISTBASE/$DISTNAME already exists!"; }
-
-cd "$DISTBASE"
-mv "$DISTPREFIX/$TMP/${REPOS_NAME}-${IDENT}" "$DISTNAME"
-purge_tmp
-
-cd "$DISTNAME" || fail "No dist directory: $DISTBASE/$DISTNAME"
-
-
-# prepare dist for release
-
-echo "###"
-echo "### Preparing distribution $DISTNAME"
-echo "###"
-
-rm -f .hgignore
-find . "(" -name \*.thy -o -name \*.ML -o -name \*.scala ")" -perm +111 -print | xargs chmod -f -x
-find . -print | xargs chmod -f u+rw
-
-perl -pi -e 's/^(ISABELLE_SCALA_BUILD_OPTIONS=")/$1-optimise /,' etc/settings
-
-./Admin/build all || fail "Failed to build distribution"
-
-cp -a src/Doc src/Doc.orig
-# FIXME
-# ./bin/isabelle build_doc -a || fail "Failed to build documentation"
-
-if [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then
-  [ -d "$ISABELLE_JEDIT_BUILD_HOME" ] || fail "Bad jedit_build component directory: \"$ISABELLE_JEDIT_BUILD_HOME\""
-  eval "$(fgrep ISABELLE_JEDIT_BUILD_VERSION "$ISABELLE_JEDIT_BUILD_HOME/etc/settings")"
-  [ -n "$ISABELLE_JEDIT_BUILD_VERSION" ] || fail "Bad ISABELLE_JEDIT_BUILD_VERSION"
-  export ISABELLE_JEDIT_BUILD_HOME ISABELLE_JEDIT_BUILD_VERSION
-  ./bin/isabelle jedit -b || fail "Failed to build Isabelle/jEdit"
-fi
-
-rm -rf Admin
-rm -rf src/Doc
-
-mv src/Doc.orig src/Doc
-
-mkdir -p contrib
-cat >contrib/README <<EOF
-This directory contains add-on components that contribute to the main
-Isabelle distribution.  Separate licensing conditions apply, see each
-directory individually.
-EOF
-
-if [ -z "$RELEASE" ]; then
-  {
-    echo
-    echo "IMPORTANT NOTE"
-    echo "=============="
-    echo
-    echo "This is an unofficial snapshot of Isabelle, created by $LOGNAME $DATE."
-    echo "See $REPOS/log/$IDENT for details."
-    echo
-  } >ANNOUNCE
-else
-  perl -pi -e "s,val is_official = false,val is_official = true,g" src/Pure/ROOT.ML
-fi
-
-perl -pi -e "s,ISABELLE_ID=\"\",ISABELLE_ID=\"$IDENT\",g" lib/scripts/getsettings
-perl -pi -e "s,ISABELLE_IDENTIFIER=\"\",ISABELLE_IDENTIFIER=\"$DISTNAME\",g" lib/scripts/getsettings
-perl -pi -e "s,{ISABELLE},$DISTNAME,g" lib/html/library_index_header.template
-perl -pi -e "s,unidentified repository version,$DISTVERSION,g" src/Pure/ROOT.ML lib/Tools/version
-perl -pi -e "s,some unidentified repository version of Isabelle,$DISTVERSION,g" README
-
-
-# create archive
-
-echo "###"
-echo "### Creating archive ..."
-echo "###"
-
-cd "$DISTBASE"
-
-echo "$DISTBASE/$DISTNAME.tar.gz" > ../ISABELLE_DIST
-echo "$IDENT" >../ISABELLE_IDENT
-
-chown -R "$LOGNAME" "$DISTNAME"
-chmod -R u+w "$DISTNAME"
-chmod -R g=o "$DISTNAME"
-chgrp -R isabelle "$DISTNAME"
-
-echo "$DISTNAME.tar.gz"
-tar -czf "$DISTNAME.tar.gz" "$DISTNAME"
-
-
-# cleanup dist
-
-mv "$DISTNAME" "${DISTNAME}-old"
-mkdir "$DISTNAME"
-
-mv "${DISTNAME}-old/README" "${DISTNAME}-old/NEWS" "${DISTNAME}-old/ANNOUNCE" \
-  "${DISTNAME}-old/COPYRIGHT" "${DISTNAME}-old/CONTRIBUTORS" "$DISTNAME"
-mkdir "$DISTNAME/doc"
-mv "${DISTNAME}-old/doc/"*.pdf "${DISTNAME}-old/doc/Contents" "$DISTNAME/doc"
-
-rm -f Isabelle && ln -sf "$DISTNAME" Isabelle
-
-chgrp -R isabelle "$DISTNAME"
-
-rm -rf "${DISTNAME}-old"
-
-echo "DONE"
diff -r 09a9761cf5ae -r 3a324a3f4aea Admin/isatest/isatest-makedist
--- a/Admin/isatest/isatest-makedist	Wed Aug 29 21:01:05 2012 +0200
+++ b/Admin/isatest/isatest-makedist	Wed Aug 29 21:20:46 2012 +0200
@@ -5,12 +5,11 @@
 # DESCRIPTION: Build distribution and run isatest-make for lots of platforms.
 
 ## global settings
-. ~/admin/isatest/isatest-settings
+. "$HOME/hg-isabelle/Admin/isatest/isatest-settings"
 
 TMP=/tmp/isatest-makedist.$$
 MAIL=$HOME/bin/pmail
 
-MAKEDIST=$HOME/bin/makedist
 MAKEALL=$HOME/bin/isatest-makeall
 TAR=tar
 
@@ -60,7 +59,7 @@
 
 echo "### building distribution"  >> $DISTLOG 2>&1
 mkdir -p $DISTPREFIX
-$MAKEDIST -j "/home/isabelle/contrib/jedit_build-20120813" >> $DISTLOG 2>&1
+"$HOME/hg-isabelle/bin/isabelle" makedist >> $DISTLOG 2>&1
 
 if [ $? -ne 0 ]
 then
diff -r 09a9761cf5ae -r 3a324a3f4aea Admin/lib/Tools/makedist
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/lib/Tools/makedist	Wed Aug 29 21:20:46 2012 +0200
@@ -0,0 +1,219 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# DESCRIPTION: make Isabelle distribution from repository
+
+## global parameters
+
+umask 022
+
+HG="${HG:-hg}"
+
+DISTPREFIX="${DISTPREFIX:-$HOME/tmp/isadist}"
+
+
+## diagnostics
+
+PRG="$(basename "$0")"
+
+function usage()
+{
+  echo
+  echo "Usage: isabelle $PRG [OPTIONS] [VERSION]"
+  echo
+  echo "  Options are:"
+  echo "    -d DIR       global directory prefix (default: \"$DISTPREFIX\")"
+  echo "    -j INT       maximum number of parallel jobs (default 1)"
+  echo "    -r RELEASE   proper release with name"
+  echo
+  echo "  Make Isabelle distribution from the local repository clone."
+  echo
+  echo "  VERSION identifies the snapshot, using usual Mercurial terminology;"
+  echo "  the default is RELEASE if given, otherwise \"tip\"."
+  echo
+  echo "  Auxiliary components are that of the running Isabelle version!"
+  echo
+  exit 1
+}
+
+function fail()
+{
+  echo "$1" >&2
+  exit 2
+}
+
+function check_number()
+{
+  [ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\""
+}
+
+
+## process command line
+
+# options
+
+JOBS=""
+RELEASE=""
+
+while getopts "d:j:r:" OPT
+do
+  case "$OPT" in
+    d)
+      DISTPREFIX="$OPTARG"
+      ;;
+    j)
+      check_number "$OPTARG"
+      JOBS="-j $OPTARG"
+      ;;
+    r)
+      RELEASE="$OPTARG"
+      ;;
+    \?)
+      usage
+      ;;
+  esac
+done
+
+shift $(($OPTIND - 1))
+
+
+# args
+
+VERSION=""
+[ "$#" -gt 0 ] && { VERSION="$1"; shift; }
+[ -z "$VERSION" ] && VERSION="$RELEASE"
+[ -z "$VERSION" ] && VERSION="tip"
+
+[ "$#" -gt 0 ] && usage
+
+IDENT=$("$HG" --repository "$ISABELLE_HOME" id -r "$VERSION" -i)
+[ -z "$IDENT" ] && fail "Bad repository version: \"$VERSION\""
+
+
+## main
+
+# dist name
+
+DATE=$(env LC_ALL=C date "+%d-%b-%Y")
+DISTDATE=$(env LC_ALL=C date "+%B %Y")
+
+if [ -z "$RELEASE" ]; then
+  DISTNAME="Isabelle_$DATE"
+  DISTVERSION="Isabelle repository snapshot $IDENT $DATE"
+else
+  DISTNAME="$RELEASE"
+  DISTVERSION="$DISTNAME: $DISTDATE"
+fi
+
+DISTBASE="$DISTPREFIX/dist-$DISTNAME"
+mkdir -p "$DISTBASE" || fail "Unable to create distribution base dir \"$DISTBASE\""
+
+DIR="$DISTBASE/$DISTNAME"
+[ -e "$DIR" ] && fail "Directory \"$DIR\" already exists"
+
+
+# retrieve repository archive
+
+echo "### Retrieving Mercurial repository $VERSION"
+
+"$HG" --repository "$ISABELLE_HOME" archive --type files -r "$IDENT" "$DIR" || \
+  fail "Failed to retrieve $VERSION"
+
+rm -f "$DIR/.hg_archival.txt"
+rm -f "$DIR/.hgtags"
+rm -f "$DIR/.hgignore"
+rm -f "$DIR/README_REPOSITORY"
+
+
+# partial context switch to new version
+
+cd "$DIR"
+
+unset ISABELLE_SETTINGS_PRESENT
+unset ISABELLE_SITE_SETTINGS_PRESENT
+
+if [ -z "$RELEASE" ]; then
+  {
+    echo
+    echo "IMPORTANT NOTE"
+    echo "=============="
+    echo
+    echo "This is snapshot of Isabelle/${IDENT} from the repository."
+    echo
+  } >ANNOUNCE
+else
+  perl -pi -e "s,val is_official = false,val is_official = true,g" src/Pure/ROOT.ML
+fi
+
+perl -pi -e "s,ISABELLE_ID=\"\",ISABELLE_ID=\"$IDENT\",g" lib/scripts/getsettings
+perl -pi -e "s,ISABELLE_IDENTIFIER=\"\",ISABELLE_IDENTIFIER=\"$DISTNAME\",g" lib/scripts/getsettings
+perl -pi -e "s,{ISABELLE},$DISTNAME,g" lib/html/library_index_header.template
+perl -pi -e "s,unidentified repository version,$DISTVERSION,g" src/Pure/ROOT.ML lib/Tools/version
+perl -pi -e "s,some unidentified repository version of Isabelle,$DISTVERSION,g" README
+
+mkdir -p contrib
+cat >contrib/README <<EOF
+This directory contains add-on components that contribute to the main
+Isabelle distribution.  Separate licensing conditions apply, see each
+directory individually.
+EOF
+
+
+# prepare dist for release
+
+echo "### Preparing distribution $DISTNAME"
+
+find . "(" -name \*.thy -o -name \*.ML -o -name \*.scala ")" -perm +111 -print | xargs chmod -f -x
+find . -print | xargs chmod -f u+rw
+
+./bin/isabelle env ISABELLE_SCALA_BUILD_OPTIONS="$ISABELLE_SCALA_BUILD_OPTIONS -optimise" \
+  ./Admin/build all || fail "Failed to build distribution"
+
+if [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then
+  ./bin/isabelle env ISABELLE_SCALA_BUILD_OPTIONS="$ISABELLE_SCALA_BUILD_OPTIONS -optimise" \
+    ./bin/isabelle jedit -b || fail "Failed to build Isabelle/jEdit"
+else
+  echo "### Missing jEdit build component"
+fi
+
+cp -a src/Doc src/Doc.orig
+./bin/isabelle env ./bin/isabelle build_doc -a || fail "Failed to build documentation"
+rm -rf src/Doc
+mv src/Doc.orig src/Doc
+
+rm -rf Admin
+
+
+# create archive
+
+echo "### Creating archive"
+
+cd "$DISTBASE"
+
+echo "$DISTBASE/$DISTNAME.tar.gz" > ../ISABELLE_DIST
+echo "$IDENT" >../ISABELLE_IDENT
+
+chown -R "$LOGNAME" "$DISTNAME"
+chmod -R u+w "$DISTNAME"
+chmod -R g=o "$DISTNAME"
+
+echo "$DISTNAME.tar.gz"
+tar -czf "$DISTNAME.tar.gz" "$DISTNAME"
+
+
+# cleanup dist
+
+mv "$DISTNAME" "${DISTNAME}-old"
+mkdir "$DISTNAME"
+
+mv "${DISTNAME}-old/README" "${DISTNAME}-old/NEWS" "${DISTNAME}-old/ANNOUNCE" \
+  "${DISTNAME}-old/COPYRIGHT" "${DISTNAME}-old/CONTRIBUTORS" "$DISTNAME"
+mkdir "$DISTNAME/doc"
+mv "${DISTNAME}-old/doc/"*.pdf "${DISTNAME}-old/doc/Contents" "$DISTNAME/doc"
+
+rm -f Isabelle && ln -sf "$DISTNAME" Isabelle
+
+rm -rf "${DISTNAME}-old"
+
+echo "DONE"
diff -r 09a9761cf5ae -r 3a324a3f4aea lib/browser/build
--- a/lib/browser/build	Wed Aug 29 21:01:05 2012 +0200
+++ b/lib/browser/build	Wed Aug 29 21:20:46 2012 +0200
@@ -59,9 +59,7 @@
 
 if [ "$OUTDATED" = true ]
 then
-  echo "###"
   echo "### Building graph browser ..."
-  echo "###"
 
   rm -rf classes && mkdir classes