--- a/Admin/lib/Tools/build_doc Mon Aug 26 14:14:33 2013 +0200
+++ b/Admin/lib/Tools/build_doc Mon Aug 26 17:37:32 2013 +0200
@@ -17,6 +17,7 @@
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
@@ -37,12 +38,14 @@
## process command line
+declare -a BUILD_ARGS=()
+
+
# options
ALL_DOCS="false"
-JOBS=""
-while getopts "aj:" OPT
+while getopts "aj:s" OPT
do
case "$OPT" in
a)
@@ -50,7 +53,11 @@
;;
j)
check_number "$OPTARG"
- JOBS="-j $OPTARG"
+ BUILD_ARGS["${#BUILD_ARGS[@]}"]="-j"
+ BUILD_ARGS["${#BUILD_ARGS[@]}"]="$OPTARG"
+ ;;
+ s)
+ BUILD_ARGS["${#BUILD_ARGS[@]}"]="-s"
;;
\?)
usage
@@ -64,9 +71,9 @@
# arguments
if [ "$ALL_DOCS" = true ]; then
- declare -a BUILD_ARGS=(-g doc)
+ BUILD_ARGS["${#BUILD_ARGS[@]}"]="-g"
+ BUILD_ARGS["${#BUILD_ARGS[@]}"]="doc"
else
- declare -a BUILD_ARGS=()
[ "$#" -eq 0 ] && usage
fi
@@ -83,12 +90,12 @@
OUTPUT="$ISABELLE_TMP_PREFIX$$"
mkdir -p "$OUTPUT" || fail "Bad directory: \"$OUTPUT\""
-"$ISABELLE_TOOL" build -R -b $JOBS "${BUILD_ARGS[@]}"
+"$ISABELLE_TOOL" build -R -b "${BUILD_ARGS[@]}"
RC=$?
if [ "$RC" = 0 ]; then
"$ISABELLE_TOOL" build -o browser_info=false -o "document=pdf" \
- -o "document_output=$OUTPUT" -c $JOBS "${BUILD_ARGS[@]}"
+ -o "document_output=$OUTPUT" -c "${BUILD_ARGS[@]}"
RC=$?
fi
--- a/Admin/lib/Tools/makedist Mon Aug 26 14:14:33 2013 +0200
+++ b/Admin/lib/Tools/makedist Mon Aug 26 17:37:32 2013 +0200
@@ -176,11 +176,11 @@
cp -a src src.orig
env ISABELLE_IDENTIFIER="${DISTNAME}-build" \
- ./bin/isabelle build_doc $JOBS -a || fail "Failed to build documentation"
+ ./bin/isabelle build_doc $JOBS -s -a || fail "Failed to build documentation"
rm -rf src
mv src.orig src
-rm -rf Admin
+rm -rf Admin browser_info heaps
# create archive
--- a/src/HOL/Tools/Lifting/lifting_def.ML Mon Aug 26 14:14:33 2013 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Mon Aug 26 17:37:32 2013 +0200
@@ -406,7 +406,7 @@
val absrep_trm = quot_thm_abs quot_thm
val rty_forced = (domain_type o fastype_of) absrep_trm
val forced_rhs = force_rty_type lthy rty_forced rhs
- val lhs = Free (Binding.print (#1 var), qty)
+ val lhs = Free (Binding.name_of (#1 var), qty)
val prop = Logic.mk_equals (lhs, absrep_trm $ forced_rhs)
val (_, prop') = Local_Defs.cert_def lthy prop
val (_, newrhs) = Local_Defs.abs_def prop'
@@ -414,7 +414,7 @@
val ((_, (_ , def_thm)), lthy') =
Local_Theory.define (var, ((Thm.def_binding (#1 var), []), newrhs)) lthy
- val transfer_rule = generate_transfer_rule lthy quot_thm rsp_thm def_thm opt_par_thm
+ val transfer_rule = generate_transfer_rule lthy' quot_thm rsp_thm def_thm opt_par_thm
val abs_eq_thm = generate_abs_eq lthy' def_thm rsp_thm quot_thm
val opt_rep_eq_thm = generate_rep_eq lthy' def_thm rsp_thm (rty_forced, qty)
--- a/src/Pure/more_thm.ML Mon Aug 26 14:14:33 2013 +0200
+++ b/src/Pure/more_thm.ML Mon Aug 26 17:37:32 2013 +0200
@@ -407,7 +407,7 @@
fun mixed_attribute f (x, th) = let val (x', th') = f (x, th) in (SOME x', SOME th') end;
fun apply_attribute (att: attribute) th x =
- let val (x', th') = att (x, th)
+ let val (x', th') = att (x, Thm.transfer (Context.theory_of x) th)
in (the_default th th', the_default x x') end;
fun attribute_declaration att th x = #2 (apply_attribute att th x);