1.1 --- a/Admin/makebundle Fri Jun 04 16:55:25 2010 +0200
1.2 +++ b/Admin/makebundle Fri Jun 04 17:27:45 2010 +0200
1.3 @@ -2,11 +2,6 @@
1.4 #
1.5 # makebundle -- re-package with add-on components
1.6
1.7 -## global settings
1.8 -
1.9 -TMP="/var/tmp/isabelle-makebundle$$"
1.10 -
1.11 -
1.12 ## diagnostics
1.13
1.14 PRG=$(basename "$0")
1.15 @@ -14,9 +9,10 @@
1.16 function usage()
1.17 {
1.18 echo
1.19 - echo "Usage: $PRG ARCHIVE COMPONENTS"
1.20 + echo "Usage: $PRG ARCHIVE PLATFORM"
1.21 echo
1.22 - echo " Re-package Isabelle distribution with add-on components."
1.23 + echo " Re-package Isabelle source distribution with add-on components"
1.24 + echo " and logic images"
1.25 echo
1.26 exit 1
1.27 }
1.28 @@ -28,34 +24,37 @@
1.29 }
1.30
1.31
1.32 -## process command line
1.33 +## implicit and explicit arguments
1.34
1.35 -[ "$#" -lt 1 ] && usage
1.36 +TMP="/var/tmp/isabelle-makebundle$$"
1.37 +mkdir "$TMP" || fail "Cannot create directory $TMP"
1.38 +
1.39 +LOGICS="HOL HOL-Nominal HOLCF ZF"
1.40 +
1.41 +[ "$#" -ne 2 ] && usage
1.42
1.43 ARCHIVE="$1"; shift
1.44 +PLATFORM="$1"; shift
1.45
1.46 -declare -a COMPONENTS
1.47 -COMPONENTS=("$@")
1.48 +[ -f "$ARCHIVE" ] || fail "Bad source archive: $ARCHIVE"
1.49
1.50
1.51 ## main
1.52
1.53 -mkdir "$TMP" || fail "Cannot create directory $TMP"
1.54 -
1.55 ARCHIVE_DIR="$(cd $(dirname "$ARCHIVE"); echo "$PWD")"
1.56 ISABELLE_NAME="$(basename "$ARCHIVE" .tar.gz)"
1.57 ISABELLE_HOME="$TMP/$ISABELLE_NAME"
1.58
1.59 -[ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE"
1.60 tar -C "$TMP" -x -z -f "$ARCHIVE"
1.61
1.62 +
1.63 echo "#bundled components" >> "$ISABELLE_HOME/etc/components"
1.64
1.65 -for COMPONENT in "${COMPONENTS[@]}"
1.66 +for CONTRIB in "$ARCHIVE_DIR"/contrib/*.tar.gz
1.67 do
1.68 - tar -C "$ISABELLE_HOME/contrib" -x -z -f "$COMPONENT"
1.69 - NAME="$(basename "$COMPONENT" .tar.gz)"
1.70 - [ -d "$ISABELLE_HOME/contrib/$NAME" ] || fail "Bad archive content $COMPONENT"
1.71 + tar -C "$ISABELLE_HOME/contrib" -x -z -f "$CONTRIB"
1.72 + NAME="$(basename "$CONTRIB" .tar.gz)"
1.73 + [ -d "$ISABELLE_HOME/contrib/$NAME" ] || fail "Bad archive content $CONTRIB"
1.74
1.75 if [ -e "$ISABELLE_HOME/contrib/$NAME/etc/settings" ]; then
1.76 echo "component $NAME"
1.77 @@ -65,9 +64,20 @@
1.78 fi
1.79 done
1.80
1.81 -tar -C "$TMP" -c -z \
1.82 - -f "${ARCHIVE_DIR}/${ISABELLE_NAME}_bundle.tar.gz" \
1.83 - Isabelle "$ISABELLE_NAME"
1.84 +
1.85 +for LOGIC in $LOGICS
1.86 +do
1.87 + LOGIC_ARCHIVE="$ARCHIVE_DIR/${LOGIC}_${PLATFORM}.tar.gz"
1.88 + [ -f "$LOGIC_ARCHIVE" ] || fail "Bad logic archive: $LOGIC_ARCHIVE"
1.89 + echo "logic $LOGIC"
1.90 + tar -C "$ISABELLE_HOME" -x -z -f "$LOGIC_ARCHIVE"
1.91 +done
1.92 +
1.93 +
1.94 +BUNDLE_ARCHIVE="${ARCHIVE_DIR}/${ISABELLE_NAME}_bundle_${PLATFORM}.tar.gz"
1.95 +
1.96 +echo "$(basename "$BUNDLE_ARCHIVE")"
1.97 +tar -C "$TMP" -c -z -f "$BUNDLE_ARCHIVE" Isabelle "$ISABELLE_NAME"
1.98
1.99
1.100 # clean up
2.1 --- a/src/Pure/Isar/expression.ML Fri Jun 04 16:55:25 2010 +0200
2.2 +++ b/src/Pure/Isar/expression.ML Fri Jun 04 17:27:45 2010 +0200
2.3 @@ -732,18 +732,20 @@
2.4 prep_decl raw_import I raw_body (ProofContext.init_global thy);
2.5 val text as (((_, exts'), _), defs) = eval ctxt' deps body_elems;
2.6
2.7 + val extraTs =
2.8 + subtract (op =) (fold Term.add_tfreesT (map snd parms) []) (fold Term.add_tfrees exts' []);
2.9 + val _ =
2.10 + if null extraTs then ()
2.11 + else warning ("Additional type variable(s) in locale specification " ^
2.12 + quote (Binding.str_of binding) ^ ": " ^
2.13 + commas (map (Syntax.string_of_typ ctxt' o TFree) (sort_wrt #1 extraTs)));
2.14 +
2.15 val predicate_binding =
2.16 if Binding.is_empty raw_predicate_binding then binding
2.17 else raw_predicate_binding;
2.18 val ((a_statement, a_intro, a_axioms), (b_statement, b_intro, b_axioms), thy') =
2.19 define_preds predicate_binding parms text thy;
2.20
2.21 - val extraTs = subtract (op =) (fold Term.add_tfreesT (map snd parms) []) (fold Term.add_tfrees exts' []);
2.22 - val _ =
2.23 - if null extraTs then ()
2.24 - else warning ("Additional type variable(s) in locale specification " ^
2.25 - quote (Binding.str_of binding));
2.26 -
2.27 val a_satisfy = Element.satisfy_morphism a_axioms;
2.28 val b_satisfy = Element.satisfy_morphism b_axioms;
2.29
3.1 --- a/src/Pure/Isar/theory_target.ML Fri Jun 04 16:55:25 2010 +0200
3.2 +++ b/src/Pure/Isar/theory_target.ML Fri Jun 04 17:27:45 2010 +0200
3.3 @@ -180,13 +180,35 @@
3.4 end;
3.5
3.6
3.7 -(* consts *)
3.8 +(* mixfix notation *)
3.9 +
3.10 +local
3.11
3.12 fun fork_mixfix (Target {is_locale, is_class, ...}) mx =
3.13 if not is_locale then (NoSyn, NoSyn, mx)
3.14 else if not is_class then (NoSyn, mx, NoSyn)
3.15 else (mx, NoSyn, NoSyn);
3.16
3.17 +in
3.18 +
3.19 +fun prep_mixfix ctxt ta (b, extra_tfrees) mx =
3.20 + let
3.21 + val mx' =
3.22 + if null extra_tfrees then mx
3.23 + else
3.24 + (warning
3.25 + ("Additional type variable(s) in specification of " ^ Binding.str_of b ^ ": " ^
3.26 + commas (map (Syntax.string_of_typ ctxt o TFree) (sort_wrt #1 extra_tfrees)) ^
3.27 + (if mx = NoSyn then ""
3.28 + else "\nDropping mixfix syntax " ^ Pretty.string_of (Syntax.pretty_mixfix mx)));
3.29 + NoSyn);
3.30 + in fork_mixfix ta mx' end;
3.31 +
3.32 +end;
3.33 +
3.34 +
3.35 +(* consts *)
3.36 +
3.37 fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) phi =
3.38 let
3.39 val b' = Morphism.binding phi b;
3.40 @@ -218,10 +240,14 @@
3.41 val thy_ctxt = ProofContext.init_global (ProofContext.theory_of lthy);
3.42 val target_ctxt = Local_Theory.target_of lthy;
3.43
3.44 - val (mx1, mx2, mx3) = fork_mixfix ta mx;
3.45 val t' = Assumption.export_term lthy target_ctxt t;
3.46 val xs = map Free (rev (Variable.add_fixed target_ctxt t' []));
3.47 val u = fold_rev lambda xs t';
3.48 +
3.49 + val extra_tfrees =
3.50 + subtract (op =) (Term.add_tfreesT (Term.fastype_of u) []) (Term.add_tfrees u []);
3.51 + val (mx1, mx2, mx3) = prep_mixfix lthy ta (b, extra_tfrees) mx;
3.52 +
3.53 val global_rhs =
3.54 singleton (Variable.export_terms (Variable.declare_term u target_ctxt) thy_ctxt) u;
3.55 in
3.56 @@ -261,7 +287,7 @@
3.57 val params = type_params @ term_params;
3.58
3.59 val U = map Term.fastype_of params ---> T;
3.60 - val (mx1, mx2, mx3) = fork_mixfix ta mx;
3.61 + val (mx1, mx2, mx3) = prep_mixfix lthy ta (b, extra_tfrees) mx;
3.62 val (const, lthy') = lthy |>
3.63 (case Class_Target.instantiation_param lthy b of
3.64 SOME c' =>
3.65 @@ -299,10 +325,7 @@
3.66 val xs = Variable.add_fixed (Local_Theory.target_of lthy) rhs' [];
3.67 val T = Term.fastype_of rhs;
3.68 val tfreesT = Term.add_tfreesT T (fold (Term.add_tfreesT o #2) xs []);
3.69 - val extra_tfrees =
3.70 - fold_types (fold_atyps
3.71 - (fn TFree v => if member (op =) tfreesT v then I else insert (op =) v | _ => I)) rhs []
3.72 - |> sort_wrt #1;
3.73 + val extra_tfrees = rev (subtract (op =) tfreesT (Term.add_tfrees rhs []));
3.74
3.75 (*const*)
3.76 val ((lhs, local_def), lthy2) = lthy |> declare_const ta extra_tfrees xs ((b, T), mx);