# HG changeset patch
# User wenzelm
# Date 1358277721 -3600
# Node ID 8226f9a1273abf60f6669205305f6e9ffe4961bc
# Parent  ebd9b82537e08f9babe581120e60f11202eadaa9# Parent  cb2b940e2fdf429827ccb1f49a6d42ec9190a4be
merged

diff -r ebd9b82537e0 -r 8226f9a1273a Admin/Release/CHECKLIST
--- a/Admin/Release/CHECKLIST	Tue Jan 15 08:29:56 2013 -0800
+++ b/Admin/Release/CHECKLIST	Tue Jan 15 20:22:01 2013 +0100
@@ -53,11 +53,7 @@
 Packaging
 =========
 
-- hg up -r DISTNAME && isabelle makedist -r DISTNAME
-
-- isabelle makedist_bundles
-
-- ./makedist_library DISTNAME_linux.tar.gz
+- hg up -r DISTNAME && Admin/Release/build -r DISTNAME /home/isabelle/dist
 
 - Mac OS X: hdiutil create -srcfolder DIR DMG
 
diff -r ebd9b82537e0 -r 8226f9a1273a Admin/Release/build
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/Release/build	Tue Jan 15 20:22:01 2013 +0100
@@ -0,0 +1,107 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# build full Isabelle distribution from repository
+
+THIS="$(cd "$(dirname "$0")"; pwd)"
+PRG="$(basename "$0")"
+
+
+## diagnostics
+
+PRG="$(basename "$0")"
+
+function usage()
+{
+  echo
+  echo "Usage: isabelle $PRG [OPTIONS] DIR [VERSION]"
+  echo
+  echo "  Options are:"
+  echo "    -j INT       maximum number of parallel jobs (default 1)"
+  echo "    -r RELEASE   proper release with name"
+  echo
+  echo "  Make Isabelle distribution DIR, using the local repository clone."
+  echo
+  echo "  VERSION identifies the snapshot, using usual Mercurial terminology;"
+  echo "  the default is RELEASE if given, otherwise \"tip\"."
+  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 "j:r:" OPT
+do
+  case "$OPT" in
+    j)
+      check_number "$OPTARG"
+      JOBS="-j $OPTARG"
+      ;;
+    r)
+      RELEASE="$OPTARG"
+      ;;
+    \?)
+      usage
+      ;;
+  esac
+done
+
+shift $(($OPTIND - 1))
+
+
+# args
+
+BASE_DIR=""
+[ "$#" -gt 0 ] && { BASE_DIR="$1"; shift; }
+[ -z "$BASE_DIR" ] && usage
+
+VERSION=""
+[ "$#" -gt 0 ] && { VERSION="$1"; shift; }
+[ -z "$VERSION" ] && VERSION="$RELEASE"
+[ -z "$VERSION" ] && VERSION="tip"
+
+[ "$#" -gt 0 ] && usage
+
+
+## Isabelle settings
+
+ISABELLE_TOOL="$THIS/../../bin/isabelle"
+ISABELLE_PLATFORM_FAMILY="$("$ISABELLE_TOOL" getenv -b ISABELLE_PLATFORM_FAMILY)"
+
+
+## main
+
+if [ -z "$RELEASE" ]; then
+  DISTNAME="Isabelle_$(env LC_ALL=C date "+%d-%b-%Y")"
+  "$ISABELLE_TOOL" makedist -d "$BASE_DIR" $JOBS
+else
+  DISTNAME="$RELEASE"
+  "$ISABELLE_TOOL" makedist -d "$BASE_DIR" $JOBS -r "$RELEASE"
+fi
+[ "$?" = 0 ] || exit "$?"
+
+DISTBASE="$BASE_DIR/dist-${DISTNAME}"
+
+"$ISABELLE_TOOL" makedist_bundles "$DISTBASE/${DISTNAME}.tar.gz"
+[ "$?" = 0 ] || exit "$?"
+
+"$THIS/build_library" $JOBS "$DISTBASE/${DISTNAME}_${ISABELLE_PLATFORM_FAMILY}.tar.gz"
+
diff -r ebd9b82537e0 -r 8226f9a1273a Admin/Release/build_library
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/Release/build_library	Tue Jan 15 20:22:01 2013 +0100
@@ -0,0 +1,96 @@
+#!/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
+
+export COPYFILE_DISABLE=true
+
+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")"
+
+echo "Z3_NON_COMMERCIAL=yes" >> etc/settings
+echo "ISABELLE_FULL_TEST=true" >> etc/settings
+
+echo -n > src/Doc/ROOT
+
+env ISABELLE_IDENTIFIER="${ISABELLE_NAME}-build" \
+  ./bin/isabelle build $JOBS -s -c -a -o browser_info \
+    -o "document=pdf" -o "document_variants=document:outline=/proof,/ML"
+RC="$?"
+
+cd ..
+
+if [ "$RC" = 0 ]; then
+  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 ebd9b82537e0 -r 8226f9a1273a Admin/Release/makedist_library
--- a/Admin/Release/makedist_library	Tue Jan 15 08:29:56 2013 -0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,96 +0,0 @@
-#!/usr/bin/env bash
-#
-# makedist_library -- 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
-
-export COPYFILE_DISABLE=true
-
-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")"
-
-echo "Z3_NON_COMMERCIAL=yes" >> etc/settings
-echo "ISABELLE_FULL_TEST=true" >> etc/settings
-
-echo -n > src/Doc/ROOT
-
-env ISABELLE_IDENTIFIER="${ISABELLE_NAME}-build" \
-  ./bin/isabelle build $JOBS -s -c -a -o browser_info \
-    -o "document=pdf" -o "document_variants=document:outline=/proof,/ML"
-RC="$?"
-
-cd ..
-
-if [ "$RC" = 0 ]; then
-  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 ebd9b82537e0 -r 8226f9a1273a Admin/lib/Tools/makedist
--- a/Admin/lib/Tools/makedist	Tue Jan 15 08:29:56 2013 -0800
+++ b/Admin/lib/Tools/makedist	Tue Jan 15 20:22:01 2013 +0100
@@ -197,6 +197,7 @@
 
 echo "$DISTBASE/$DISTNAME.tar.gz"
 env COPYFILE_DISABLE=true tar -c -z -f "$DISTNAME.tar.gz" "$DISTNAME"
+[ "$?" = 0 ] || exit "$?"
 
 
 # cleanup dist
@@ -213,4 +214,3 @@
 
 rm -rf "${DISTNAME}-old"
 
-echo "DONE"
diff -r ebd9b82537e0 -r 8226f9a1273a Admin/lib/Tools/makedist_bundles
--- a/Admin/lib/Tools/makedist_bundles	Tue Jan 15 08:29:56 2013 -0800
+++ b/Admin/lib/Tools/makedist_bundles	Tue Jan 15 20:22:01 2013 +0100
@@ -177,7 +177,7 @@
 BUNDLE_ARCHIVE="${ARCHIVE_DIR}/${ISABELLE_NAME}_${PLATFORM_FAMILY}.tar.gz"
 
 echo "packaging $(basename "$BUNDLE_ARCHIVE")"
-tar -C "$TMP" -c -z -f "$BUNDLE_ARCHIVE" "$ISABELLE_NAME"
+tar -C "$TMP" -c -z -f "$BUNDLE_ARCHIVE" "$ISABELLE_NAME" || exit 2
 
 
 # clean up
diff -r ebd9b82537e0 -r 8226f9a1273a src/HOL/Matrix_LP/Cplex_tools.ML
--- a/src/HOL/Matrix_LP/Cplex_tools.ML	Tue Jan 15 08:29:56 2013 -0800
+++ b/src/HOL/Matrix_LP/Cplex_tools.ML	Tue Jan 15 20:22:01 2013 +0100
@@ -1148,7 +1148,7 @@
         result
     end
     handle (Load_cplexResult s) => raise (Execute ("Load_cplexResult: "^s^"\nExecute: "^answer))
-         | _ => raise (Execute answer)  (* FIXME avoid handle _ *)
+         | exn => if Exn.is_interrupt exn then reraise exn else raise (Execute answer)
     end
 
 fun solve_cplex prog =
diff -r ebd9b82537e0 -r 8226f9a1273a src/HOL/Tools/Quotient/quotient_def.ML
--- a/src/HOL/Tools/Quotient/quotient_def.ML	Tue Jan 15 08:29:56 2013 -0800
+++ b/src/HOL/Tools/Quotient/quotient_def.ML	Tue Jan 15 20:22:01 2013 +0100
@@ -166,10 +166,10 @@
         case lhs_eq of
           SOME (Const (@{const_name HOL.eq}, _) $ _ $ _) => SOME (@{thm refl} RS thm)
           | SOME _ => (case body_type (fastype_of lhs) of
-            Type (typ_name, _) => ( SOME
-              (#equiv_thm (the (Quotient_Info.lookup_quotients lthy typ_name)) 
-                RS @{thm Equiv_Relations.equivp_reflp} RS thm)
-              handle _ => NONE)
+            Type (typ_name, _) =>
+              try (fn () =>
+                #equiv_thm (the (Quotient_Info.lookup_quotients lthy typ_name)) 
+                  RS @{thm Equiv_Relations.equivp_reflp} RS thm) ()
             | _ => NONE
             )
           | _ => NONE
diff -r ebd9b82537e0 -r 8226f9a1273a src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML	Tue Jan 15 08:29:56 2013 -0800
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML	Tue Jan 15 20:22:01 2013 +0100
@@ -68,8 +68,8 @@
       val metis_fail = ref false
     in
       fun handle_metis_fail try_metis () =
-        try_metis () handle exp =>
-          (if Exn.is_interrupt exp orelse debug then reraise exp 
+        try_metis () handle exn =>
+          (if Exn.is_interrupt exn orelse debug then reraise exn
            else metis_fail := true; SOME Time.zeroTime)
       fun get_time lazy_time =
         if !metis_fail then SOME Time.zeroTime else Lazy.force lazy_time
diff -r ebd9b82537e0 -r 8226f9a1273a src/HOL/Word/WordBitwise.thy
--- a/src/HOL/Word/WordBitwise.thy	Tue Jan 15 08:29:56 2013 -0800
+++ b/src/HOL/Word/WordBitwise.thy	Tue Jan 15 20:22:01 2013 +0100
@@ -514,10 +514,12 @@
       |> mk_nat_clist;
     val prop = Thm.mk_binop @{cterm "op = :: nat list => _"} ct ns
                  |> Thm.apply @{cterm Trueprop};
-  in Goal.prove_internal [] prop 
-      (K (REPEAT_DETERM (resolve_tac @{thms upt_eq_list_intros} 1
-          ORELSE simp_tac word_ss 1))) |> mk_meta_eq |> SOME end
-    handle TERM _ => NONE
+  in
+    try (fn () =>
+      Goal.prove_internal [] prop 
+        (K (REPEAT_DETERM (resolve_tac @{thms upt_eq_list_intros} 1
+            ORELSE simp_tac word_ss 1))) |> mk_meta_eq) ()
+  end
   | _ => NONE;
 
 val expand_upt_simproc = Simplifier.make_simproc
diff -r ebd9b82537e0 -r 8226f9a1273a src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Tue Jan 15 08:29:56 2013 -0800
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Tue Jan 15 20:22:01 2013 +0100
@@ -86,22 +86,24 @@
     {
       nodes_status.get(node_name) match {
         case Some(st) if st.total > 0 =>
+          val colors = List(
+            (st.unprocessed, PIDE.options.color_value("unprocessed1_color")),
+            (st.running, PIDE.options.color_value("running_color")),
+            (st.warned, PIDE.options.color_value("warning_color")),
+            (st.failed, PIDE.options.color_value("error_color")))
+
           val size = peer.getSize()
           val insets = border.getBorderInsets(this.peer)
           val w = size.width - insets.left - insets.right
           val h = size.height - insets.top - insets.bottom
           var end = size.width - insets.right
-          for {
-            (n, color) <- List(
-              (st.unprocessed, PIDE.options.color_value("unprocessed1_color")),
-              (st.running, PIDE.options.color_value("running_color")),
-              (st.warned, PIDE.options.color_value("warning_color")),
-              (st.failed, PIDE.options.color_value("error_color"))) }
+
+          for { (n, color) <- colors }
           {
             gfx.setColor(color)
-            val v = (n * w / st.total) max (if (n > 0) 4 else 0)
+            val v = (n * (w - colors.length) / st.total) max (if (n > 0) 4 else 0)
             gfx.fillRect(end - v, insets.top, v, h)
-            end -= v
+            end = end - v - 1
           }
         case _ =>
       }