# 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 _ => }