--- a/Admin/makebundle Fri Jun 04 16:55:25 2010 +0200
+++ b/Admin/makebundle Fri Jun 04 17:27:45 2010 +0200
@@ -2,11 +2,6 @@
#
# makebundle -- re-package with add-on components
-## global settings
-
-TMP="/var/tmp/isabelle-makebundle$$"
-
-
## diagnostics
PRG=$(basename "$0")
@@ -14,9 +9,10 @@
function usage()
{
echo
- echo "Usage: $PRG ARCHIVE COMPONENTS"
+ echo "Usage: $PRG ARCHIVE PLATFORM"
echo
- echo " Re-package Isabelle distribution with add-on components."
+ echo " Re-package Isabelle source distribution with add-on components"
+ echo " and logic images"
echo
exit 1
}
@@ -28,34 +24,37 @@
}
-## process command line
+## implicit and explicit arguments
-[ "$#" -lt 1 ] && usage
+TMP="/var/tmp/isabelle-makebundle$$"
+mkdir "$TMP" || fail "Cannot create directory $TMP"
+
+LOGICS="HOL HOL-Nominal HOLCF ZF"
+
+[ "$#" -ne 2 ] && usage
ARCHIVE="$1"; shift
+PLATFORM="$1"; shift
-declare -a COMPONENTS
-COMPONENTS=("$@")
+[ -f "$ARCHIVE" ] || fail "Bad source archive: $ARCHIVE"
## main
-mkdir "$TMP" || fail "Cannot create directory $TMP"
-
ARCHIVE_DIR="$(cd $(dirname "$ARCHIVE"); echo "$PWD")"
ISABELLE_NAME="$(basename "$ARCHIVE" .tar.gz)"
ISABELLE_HOME="$TMP/$ISABELLE_NAME"
-[ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE"
tar -C "$TMP" -x -z -f "$ARCHIVE"
+
echo "#bundled components" >> "$ISABELLE_HOME/etc/components"
-for COMPONENT in "${COMPONENTS[@]}"
+for CONTRIB in "$ARCHIVE_DIR"/contrib/*.tar.gz
do
- tar -C "$ISABELLE_HOME/contrib" -x -z -f "$COMPONENT"
- NAME="$(basename "$COMPONENT" .tar.gz)"
- [ -d "$ISABELLE_HOME/contrib/$NAME" ] || fail "Bad archive content $COMPONENT"
+ tar -C "$ISABELLE_HOME/contrib" -x -z -f "$CONTRIB"
+ NAME="$(basename "$CONTRIB" .tar.gz)"
+ [ -d "$ISABELLE_HOME/contrib/$NAME" ] || fail "Bad archive content $CONTRIB"
if [ -e "$ISABELLE_HOME/contrib/$NAME/etc/settings" ]; then
echo "component $NAME"
@@ -65,9 +64,20 @@
fi
done
-tar -C "$TMP" -c -z \
- -f "${ARCHIVE_DIR}/${ISABELLE_NAME}_bundle.tar.gz" \
- Isabelle "$ISABELLE_NAME"
+
+for LOGIC in $LOGICS
+do
+ LOGIC_ARCHIVE="$ARCHIVE_DIR/${LOGIC}_${PLATFORM}.tar.gz"
+ [ -f "$LOGIC_ARCHIVE" ] || fail "Bad logic archive: $LOGIC_ARCHIVE"
+ echo "logic $LOGIC"
+ tar -C "$ISABELLE_HOME" -x -z -f "$LOGIC_ARCHIVE"
+done
+
+
+BUNDLE_ARCHIVE="${ARCHIVE_DIR}/${ISABELLE_NAME}_bundle_${PLATFORM}.tar.gz"
+
+echo "$(basename "$BUNDLE_ARCHIVE")"
+tar -C "$TMP" -c -z -f "$BUNDLE_ARCHIVE" Isabelle "$ISABELLE_NAME"
# clean up
--- a/src/Pure/Isar/expression.ML Fri Jun 04 16:55:25 2010 +0200
+++ b/src/Pure/Isar/expression.ML Fri Jun 04 17:27:45 2010 +0200
@@ -732,18 +732,20 @@
prep_decl raw_import I raw_body (ProofContext.init_global thy);
val text as (((_, exts'), _), defs) = eval ctxt' deps body_elems;
+ val extraTs =
+ subtract (op =) (fold Term.add_tfreesT (map snd parms) []) (fold Term.add_tfrees exts' []);
+ val _ =
+ if null extraTs then ()
+ else warning ("Additional type variable(s) in locale specification " ^
+ quote (Binding.str_of binding) ^ ": " ^
+ commas (map (Syntax.string_of_typ ctxt' o TFree) (sort_wrt #1 extraTs)));
+
val predicate_binding =
if Binding.is_empty raw_predicate_binding then binding
else raw_predicate_binding;
val ((a_statement, a_intro, a_axioms), (b_statement, b_intro, b_axioms), thy') =
define_preds predicate_binding parms text thy;
- val extraTs = subtract (op =) (fold Term.add_tfreesT (map snd parms) []) (fold Term.add_tfrees exts' []);
- val _ =
- if null extraTs then ()
- else warning ("Additional type variable(s) in locale specification " ^
- quote (Binding.str_of binding));
-
val a_satisfy = Element.satisfy_morphism a_axioms;
val b_satisfy = Element.satisfy_morphism b_axioms;
--- a/src/Pure/Isar/theory_target.ML Fri Jun 04 16:55:25 2010 +0200
+++ b/src/Pure/Isar/theory_target.ML Fri Jun 04 17:27:45 2010 +0200
@@ -180,13 +180,35 @@
end;
-(* consts *)
+(* mixfix notation *)
+
+local
fun fork_mixfix (Target {is_locale, is_class, ...}) mx =
if not is_locale then (NoSyn, NoSyn, mx)
else if not is_class then (NoSyn, mx, NoSyn)
else (mx, NoSyn, NoSyn);
+in
+
+fun prep_mixfix ctxt ta (b, extra_tfrees) mx =
+ let
+ val mx' =
+ if null extra_tfrees then mx
+ else
+ (warning
+ ("Additional type variable(s) in specification of " ^ Binding.str_of b ^ ": " ^
+ commas (map (Syntax.string_of_typ ctxt o TFree) (sort_wrt #1 extra_tfrees)) ^
+ (if mx = NoSyn then ""
+ else "\nDropping mixfix syntax " ^ Pretty.string_of (Syntax.pretty_mixfix mx)));
+ NoSyn);
+ in fork_mixfix ta mx' end;
+
+end;
+
+
+(* consts *)
+
fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) phi =
let
val b' = Morphism.binding phi b;
@@ -218,10 +240,14 @@
val thy_ctxt = ProofContext.init_global (ProofContext.theory_of lthy);
val target_ctxt = Local_Theory.target_of lthy;
- val (mx1, mx2, mx3) = fork_mixfix ta mx;
val t' = Assumption.export_term lthy target_ctxt t;
val xs = map Free (rev (Variable.add_fixed target_ctxt t' []));
val u = fold_rev lambda xs t';
+
+ val extra_tfrees =
+ subtract (op =) (Term.add_tfreesT (Term.fastype_of u) []) (Term.add_tfrees u []);
+ val (mx1, mx2, mx3) = prep_mixfix lthy ta (b, extra_tfrees) mx;
+
val global_rhs =
singleton (Variable.export_terms (Variable.declare_term u target_ctxt) thy_ctxt) u;
in
@@ -261,7 +287,7 @@
val params = type_params @ term_params;
val U = map Term.fastype_of params ---> T;
- val (mx1, mx2, mx3) = fork_mixfix ta mx;
+ val (mx1, mx2, mx3) = prep_mixfix lthy ta (b, extra_tfrees) mx;
val (const, lthy') = lthy |>
(case Class_Target.instantiation_param lthy b of
SOME c' =>
@@ -299,10 +325,7 @@
val xs = Variable.add_fixed (Local_Theory.target_of lthy) rhs' [];
val T = Term.fastype_of rhs;
val tfreesT = Term.add_tfreesT T (fold (Term.add_tfreesT o #2) xs []);
- val extra_tfrees =
- fold_types (fold_atyps
- (fn TFree v => if member (op =) tfreesT v then I else insert (op =) v | _ => I)) rhs []
- |> sort_wrt #1;
+ val extra_tfrees = rev (subtract (op =) tfreesT (Term.add_tfrees rhs []));
(*const*)
val ((lhs, local_def), lthy2) = lthy |> declare_const ta extra_tfrees xs ((b, T), mx);