--- a/Admin/PLATFORMS Wed Dec 28 20:05:28 2011 +0100
+++ b/Admin/PLATFORMS Wed Dec 28 20:05:52 2011 +0100
@@ -61,21 +61,25 @@
32 bit vs. 64 bit platforms
---------------------------
-64 bit hardware becomes more and more important for many users.
-Add-on tools need to work seamlessly without manual user
-configuration, although it is often sufficient to fall back on 32 bit
-executables.
+Most users already have 64 bit hardware, and many of them are running
+a 64 bit operating system. Native 64 bit support for ML and Scala/JVM
+is increasingly important for big Isabelle applications, but 32 bit is
+often the default to get started. Add-on executables need to work
+seamlessly without manual user configuration, either as native 64 bit
+executables or in 32 bit mode on a 64 bit platform.
The ISABELLE_PLATFORM setting variable refers to the 32 bit version of
-the platform, even on 64 bit hardware. Power-tools need to indicate
-64 bit support explicitly, via the (optional) ISABELLE_PLATFORM64
-setting. The following bash expression prefers the 64 bit platform,
-if that is available:
+the platform, even on 64 bit hardware. Tools need to indicate 64 bit
+support explicitly via the (optional) ISABELLE_PLATFORM64 setting, if
+this is really required. The following bash expression prefers the 64
+bit platform, if that is available:
"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"
Note that ML and JVM may have a different idea of the platform,
-depending on the respective binaries that are actually run.
+depending on the respective binaries that are actually run. The
+"uname" Unix tool usually only tells about its own executable format,
+not the underlying platform.
Dependable system tools
--- a/Admin/isatest/isatest-makeall Wed Dec 28 20:05:28 2011 +0100
+++ b/Admin/isatest/isatest-makeall Wed Dec 28 20:05:52 2011 +0100
@@ -71,12 +71,6 @@
macbroy2)
MFLAGS="-k"
- TARGETS=full
- NICE=""
- ;;
-
- macbroy5)
- MFLAGS="-k -j 2"
NICE=""
;;
@@ -102,7 +96,6 @@
macbroy30)
MFLAGS="-k"
- TARGETS=full
NICE=""
;;
@@ -124,8 +117,13 @@
TARGETS="$2"
shift 2
ISABELLE_HOME="$($ISABELLE_TOOL getenv -b ISABELLE_HOME)"
- DIR="$ISABELLE_HOME/src/$LOGIC"
- TOOL="$ISABELLE_TOOL make $MFLAGS $TARGETS"
+ if [ "$LOGIC" = "." ]; then
+ DIR="."
+ TOOL="$ISABELLE_TOOL makeall $MFLAGS $TARGETS"
+ else
+ DIR="$ISABELLE_HOME/src/$LOGIC"
+ TOOL="$ISABELLE_TOOL make $MFLAGS $TARGETS"
+ fi
else
DIR="."
TOOL="$ISABELLE_TOOL makeall $MFLAGS $TARGETS"
--- a/Admin/isatest/isatest-makedist Wed Dec 28 20:05:28 2011 +0100
+++ b/Admin/isatest/isatest-makedist Wed Dec 28 20:05:52 2011 +0100
@@ -107,9 +107,11 @@
sleep 15
$SSH macbroy24 "$MAKEALL $HOME/settings/at64-poly"
sleep 15
-$SSH macbroy2 "$MAKEALL $HOME/settings/mac-poly64-M4; $MAKEALL $HOME/settings/mac-poly64-M8; $MAKEALL $HOME/settings/mac-poly-M4; $MAKEALL $HOME/settings/mac-poly-M8"
-sleep 15
-$SSH macbroy5 "$MAKEALL $HOME/settings/mac-poly"
+$SSH macbroy2 "
+ $MAKEALL $HOME/settings/mac-poly64-M4 -l . full;
+ $MAKEALL $HOME/settings/mac-poly64-M8 -l . full;
+ $MAKEALL $HOME/settings/mac-poly-M4;
+ $MAKEALL $HOME/settings/mac-poly-M8"
sleep 15
$SSH macbroy6 "$MAKEALL $HOME/settings/mac-poly64-M2"
sleep 15
--- a/Admin/isatest/settings/afp-poly Wed Dec 28 20:05:28 2011 +0100
+++ b/Admin/isatest/settings/afp-poly Wed Dec 28 20:05:52 2011 +0100
@@ -28,4 +28,4 @@
ISABELLE_USEDIR_OPTIONS="-i false -d false -t true -M 4 -q 2"
-init_component "$CONTRIB/kodkodi"
+#init_component "$CONTRIB/kodkodi-1.2.16"
--- a/Admin/isatest/settings/at-poly Wed Dec 28 20:05:28 2011 +0100
+++ b/Admin/isatest/settings/at-poly Wed Dec 28 20:05:52 2011 +0100
@@ -24,5 +24,5 @@
ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -t true"
-init_component "$HOME/contrib_devel/kodkodi"
+#init_component "$HOME/contrib_devel/kodkodi-1.2.16"
--- a/Admin/isatest/settings/at-poly-e Wed Dec 28 20:05:28 2011 +0100
+++ b/Admin/isatest/settings/at-poly-e Wed Dec 28 20:05:52 2011 +0100
@@ -24,4 +24,4 @@
ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -t true"
-init_component "$HOME/contrib_devel/kodkodi"
+#init_component "$HOME/contrib_devel/kodkodi-1.2.16"
--- a/Admin/isatest/settings/at-poly-test Wed Dec 28 20:05:28 2011 +0100
+++ b/Admin/isatest/settings/at-poly-test Wed Dec 28 20:05:52 2011 +0100
@@ -28,4 +28,4 @@
ISABELLE_OCAML="/home/isabelle/contrib_devel/ocaml/x86-linux/ocaml"
ISABELLE_SWIPL="/home/isabelle/contrib_devel/swipl/bin/swipl"
-init_component "$HOME/contrib_devel/kodkodi"
+#init_component "$HOME/contrib_devel/kodkodi-1.2.16"
--- a/Admin/isatest/settings/at64-poly Wed Dec 28 20:05:28 2011 +0100
+++ b/Admin/isatest/settings/at64-poly Wed Dec 28 20:05:52 2011 +0100
@@ -24,4 +24,4 @@
ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true"
-init_component "$HOME/contrib_devel/kodkodi"
+#init_component "$HOME/contrib_devel/kodkodi-1.2.16"
--- a/Admin/isatest/settings/cygwin-poly-e Wed Dec 28 20:05:28 2011 +0100
+++ b/Admin/isatest/settings/cygwin-poly-e Wed Dec 28 20:05:52 2011 +0100
@@ -24,4 +24,4 @@
ISABELLE_USEDIR_OPTIONS="-M 1 -i false -d false"
-init_component "$HOME/contrib/kodkodi"
+#init_component "$HOME/contrib/kodkodi-1.2.16"
--- a/Admin/isatest/settings/mac-poly Wed Dec 28 20:05:28 2011 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-
- POLYML_HOME="/home/polyml/polyml-5.2.1"
- ML_SYSTEM="polyml-5.2.1"
- ML_PLATFORM="ppc-darwin"
- ML_HOME="$POLYML_HOME/$ML_PLATFORM"
- ML_OPTIONS="-H 500"
-
-ISABELLE_HOME_USER=~/isabelle-mac-poly
-
-# Where to look for isabelle tools (multiple dirs separated by ':').
-ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
-
-# Location for temporary files (should be on a local file system).
-ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
-
-
-# Heap input locations. ML system identifier is included in lookup.
-ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
-
-# Heap output location. ML system identifier is appended automatically later on.
-ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
-ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
-
-ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -g false"
-
-init_component "$HOME/contrib_devel/kodkodi"
--- a/Admin/isatest/settings/mac-poly-M2 Wed Dec 28 20:05:28 2011 +0100
+++ b/Admin/isatest/settings/mac-poly-M2 Wed Dec 28 20:05:52 2011 +0100
@@ -25,5 +25,5 @@
ISABELLE_USEDIR_OPTIONS="-i false -d false -t true -M 2 -q 2"
-init_component "$HOME/contrib_devel/kodkodi"
+#init_component "$HOME/contrib_devel/kodkodi-1.2.16"
--- a/Admin/isatest/settings/mac-poly-M4 Wed Dec 28 20:05:28 2011 +0100
+++ b/Admin/isatest/settings/mac-poly-M4 Wed Dec 28 20:05:52 2011 +0100
@@ -25,4 +25,4 @@
ISABELLE_USEDIR_OPTIONS="-i false -d false -t true -M 4 -q 2"
-init_component "$HOME/contrib_devel/kodkodi"
+#init_component "$HOME/contrib_devel/kodkodi-1.2.16"
--- a/Admin/isatest/settings/mac-poly-M8 Wed Dec 28 20:05:28 2011 +0100
+++ b/Admin/isatest/settings/mac-poly-M8 Wed Dec 28 20:05:52 2011 +0100
@@ -25,5 +25,5 @@
ISABELLE_USEDIR_OPTIONS="-i false -d false -t true -M 8 -q 2"
-init_component "$HOME/contrib_devel/kodkodi"
+#init_component "$HOME/contrib_devel/kodkodi-1.2.16"
--- a/Admin/isatest/settings/mac-poly64-M2 Wed Dec 28 20:05:28 2011 +0100
+++ b/Admin/isatest/settings/mac-poly64-M2 Wed Dec 28 20:05:52 2011 +0100
@@ -25,5 +25,5 @@
ISABELLE_USEDIR_OPTIONS="-i false -d false -t true -M 2 -q 2"
-init_component "$HOME/contrib_devel/kodkodi"
+#init_component "$HOME/contrib_devel/kodkodi-1.2.16"
--- a/Admin/isatest/settings/mac-poly64-M4 Wed Dec 28 20:05:28 2011 +0100
+++ b/Admin/isatest/settings/mac-poly64-M4 Wed Dec 28 20:05:52 2011 +0100
@@ -25,4 +25,4 @@
ISABELLE_USEDIR_OPTIONS="-i false -d false -t true -M 4 -q 2"
-init_component "$HOME/contrib_devel/kodkodi"
+#init_component "$HOME/contrib_devel/kodkodi-1.2.16"
--- a/Admin/isatest/settings/mac-poly64-M8 Wed Dec 28 20:05:28 2011 +0100
+++ b/Admin/isatest/settings/mac-poly64-M8 Wed Dec 28 20:05:52 2011 +0100
@@ -25,5 +25,5 @@
ISABELLE_USEDIR_OPTIONS="-i false -d false -t true -M 8 -q 2"
-init_component "$HOME/contrib_devel/kodkodi"
+#init_component "$HOME/contrib_devel/kodkodi-1.2.16"
--- a/src/HOL/Tools/Datatype/datatype_case.ML Wed Dec 28 20:05:28 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_case.ML Wed Dec 28 20:05:52 2011 +0100
@@ -12,6 +12,7 @@
val make_case : Proof.context -> config -> string list -> term -> (term * term) list -> term
val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option
val case_tr: bool -> Proof.context -> term list -> term
+ val show_cases: bool Config.T
val case_tr': string -> Proof.context -> term list -> term
val add_case_tr' : string list -> theory -> theory
val setup: theory -> theory
@@ -414,27 +415,31 @@
(* print translation *)
+val show_cases = Attrib.setup_config_bool @{binding show_cases} (K true);
+
fun case_tr' cname ctxt ts =
- let
- fun mk_clause (pat, rhs) =
- let val xs = Term.add_frees pat [] in
- Syntax.const @{syntax_const "_case1"} $
- map_aterms
- (fn Free p => Syntax_Trans.mark_boundT p
- | Const (s, _) => Syntax.const (Lexicon.mark_const s)
- | t => t) pat $
- map_aterms
- (fn x as Free (s, T) => if member (op =) xs (s, T) then Syntax_Trans.mark_bound s else x
- | t => t) rhs
- end;
- in
- (case strip_case' ctxt true (list_comb (Syntax.const cname, ts)) of
- SOME (x, clauses) =>
- Syntax.const @{syntax_const "_case_syntax"} $ x $
- foldr1 (fn (t, u) => Syntax.const @{syntax_const "_case2"} $ t $ u)
- (map mk_clause clauses)
- | NONE => raise Match)
- end;
+ if Config.get ctxt show_cases then
+ let
+ fun mk_clause (pat, rhs) =
+ let val xs = Term.add_frees pat [] in
+ Syntax.const @{syntax_const "_case1"} $
+ map_aterms
+ (fn Free p => Syntax_Trans.mark_boundT p
+ | Const (s, _) => Syntax.const (Lexicon.mark_const s)
+ | t => t) pat $
+ map_aterms
+ (fn x as Free (s, T) => if member (op =) xs (s, T) then Syntax_Trans.mark_bound s else x
+ | t => t) rhs
+ end;
+ in
+ (case strip_case' ctxt true (list_comb (Syntax.const cname, ts)) of
+ SOME (x, clauses) =>
+ Syntax.const @{syntax_const "_case_syntax"} $ x $
+ foldr1 (fn (t, u) => Syntax.const @{syntax_const "_case2"} $ t $ u)
+ (map mk_clause clauses)
+ | NONE => raise Match)
+ end
+ else raise Match;
fun add_case_tr' case_names thy =
Sign.add_advanced_trfuns ([], [],