--- a/Admin/build Mon Nov 07 14:16:01 2011 +0100
+++ b/Admin/build Mon Nov 07 17:24:57 2011 +0100
@@ -84,7 +84,6 @@
function build_jars ()
{
- "$ISABELLE_TOOL" env "$ISABELLE_HOME/lib/scripts/java_ext_dirs" >/dev/null
pushd "$ISABELLE_HOME/src/Pure" >/dev/null
"$ISABELLE_TOOL" env ./build-jars "$@" || exit $?
popd >/dev/null
--- a/NEWS Mon Nov 07 14:16:01 2011 +0100
+++ b/NEWS Mon Nov 07 17:24:57 2011 +0100
@@ -10,22 +10,27 @@
instead. INCOMPATIBILITY.
* Ancient code generator for SML and its commands 'code_module',
- 'code_library', 'consts_code', 'types_code' have been discontinued.
- Use commands of the generic code generator instead. INCOMPATIBILITY.
-
-* Redundant attribute 'code_inline' has been discontinued. Use 'code_unfold'
-instead. INCOMPATIBILITY.
+'code_library', 'consts_code', 'types_code' have been discontinued.
+Use commands of the generic code generator instead. INCOMPATIBILITY.
+
+* Redundant attribute 'code_inline' has been discontinued. Use
+'code_unfold' instead. INCOMPATIBILITY.
+
*** HOL ***
-* 'Transitive_Closure.ntrancl': bounded transitive closure on relations.
-
-* 'Set.not_member' now qualifed. INCOMPATIBILITY.
-
-* 'sublists' moved to More_List.thy. INCOMPATIBILITY.
+* Clarified attribute "mono_set": pure declararation without modifying
+the result of the fact expression.
+
+* "Transitive_Closure.ntrancl": bounded transitive closure on
+relations.
+
+* Constant "Set.not_member" now qualifed. INCOMPATIBILITY.
+
+* "sublists" moved to theory More_List. INCOMPATIBILITY.
* Theory Int: Discontinued many legacy theorems specific to type int.
- INCOMPATIBILITY, use the corresponding generic theorems instead.
+INCOMPATIBILITY, use the corresponding generic theorems instead.
zminus_zminus ~> minus_minus
zminus_0 ~> minus_zero
@@ -62,17 +67,18 @@
zero_less_zpower_abs_iff ~> zero_less_power_abs_iff
zero_le_zpower_abs ~> zero_le_power_abs
-* New case_product attribute to generate a case rule doing multiple case
- distinctions at the same time: E.g.
-
- list.exhaust[case_product nat.exhaust]
-
- produces a rule which can be used to perform case distinction on both
- a list and a nat.
+* New "case_product" attribute to generate a case rule doing multiple
+case distinctions at the same time. E.g.
+
+ list.exhaust [case_product nat.exhaust]
+
+produces a rule which can be used to perform case distinction on both
+a list and a nat.
+
*** FOL ***
-* New case_product attribute (see HOL).
+* New "case_product" attribute (see HOL).
*** ML ***
--- a/lib/Tools/java Mon Nov 07 14:16:01 2011 +0100
+++ b/lib/Tools/java Mon Nov 07 17:24:57 2011 +0100
@@ -22,5 +22,5 @@
fi
exec "$JAVA_EXE" -Dfile.encoding=UTF-8 $SERVER \
- "-Djava.ext.dirs=$("$ISABELLE_HOME/lib/scripts/java_ext_dirs")" "$@"
+ "-Djava.ext.dirs=$("$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs")" "$@"
--- a/lib/Tools/scala Mon Nov 07 14:16:01 2011 +0100
+++ b/lib/Tools/scala Mon Nov 07 17:24:57 2011 +0100
@@ -10,4 +10,4 @@
CLASSPATH="$(jvmpath "$CLASSPATH")"
exec "$SCALA_HOME/bin/scala" -Dfile.encoding=UTF-8 \
- "-Djava.ext.dirs=$("$ISABELLE_HOME/lib/scripts/java_ext_dirs")" "$@"
+ "-Djava.ext.dirs=$("$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs")" "$@"
--- a/lib/Tools/scalac Mon Nov 07 14:16:01 2011 +0100
+++ b/lib/Tools/scalac Mon Nov 07 17:24:57 2011 +0100
@@ -10,4 +10,4 @@
CLASSPATH="$(jvmpath "$CLASSPATH")"
exec "$SCALA_HOME/bin/scalac" -Dfile.encoding=UTF-8 \
- "-Djava.ext.dirs=$("$ISABELLE_HOME/lib/scripts/java_ext_dirs")" "$@"
+ "-Djava.ext.dirs=$("$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs")" "$@"
--- a/lib/scripts/java_ext_dirs Mon Nov 07 14:16:01 2011 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,45 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# Augment Java extension directories.
-
-## diagnostics
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-
-## dependencies
-
-SOURCE="$ISABELLE_HOME/src/Pure/System/Java_Ext_Dirs.java"
-
-TARGET_DIR="$ISABELLE_HOME/lib/classes"
-TARGET="$TARGET_DIR/java_ext_dirs.jar"
-
-if [ ! -e "$TARGET" -o "$SOURCE" -nt "$TARGET" ]; then
- mkdir -p "$TARGET_DIR" || fail "Bad directory: \"$TARGET_DIR\""
- pushd "$TARGET_DIR" >/dev/null
-
- BUILD="build$$"
- TMP_JAR="java_ext_dirs$$.jar"
-
- rm -rf "$BUILD" && mkdir "$BUILD"
- javac -d "$BUILD" -source 1.5 "$(jvmpath "$SOURCE")" || fail "Failed to compile sources"
- jar cf "$TMP_JAR" -C "$BUILD" . || fail "Failed to produce $TMP_JAR"
- mv "$TMP_JAR" "$TARGET"
- rm -rf "$BUILD"
-
- popd >/dev/null
-fi
-
-
-## main
-
-JAVA_EXE="${THIS_JAVA:-$ISABELLE_JAVA}"
-exec "$JAVA_EXE" -classpath "$(jvmpath "$TARGET")" isabelle.Java_Ext_Dirs \
- "$(jvmpath "$ISABELLE_HOME/lib/classes/ext")"
-
--- a/src/HOL/Algebra/AbelCoset.thy Mon Nov 07 14:16:01 2011 +0100
+++ b/src/HOL/Algebra/AbelCoset.thy Mon Nov 07 17:24:57 2011 +0100
@@ -246,21 +246,19 @@
shows "abelian_subgroup H G"
proof -
interpret comm_group "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
- by (rule a_comm_group)
+ by (rule a_comm_group)
interpret subgroup "H" "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
- by (rule a_subgroup)
+ by (rule a_subgroup)
show "abelian_subgroup H G"
- apply unfold_locales
+ apply unfold_locales
proof (simp add: r_coset_def l_coset_def, clarsimp)
fix x
assume xcarr: "x \<in> carrier G"
- from a_subgroup
- have Hcarr: "H \<subseteq> carrier G" by (unfold subgroup_def, simp)
- from xcarr Hcarr
- show "(\<Union>h\<in>H. {h \<oplus>\<^bsub>G\<^esub> x}) = (\<Union>h\<in>H. {x \<oplus>\<^bsub>G\<^esub> h})"
- using m_comm[simplified]
- by fast
+ from a_subgroup have Hcarr: "H \<subseteq> carrier G"
+ unfolding subgroup_def by simp
+ from xcarr Hcarr show "(\<Union>h\<in>H. {h \<oplus>\<^bsub>G\<^esub> x}) = (\<Union>h\<in>H. {x \<oplus>\<^bsub>G\<^esub> h})"
+ using m_comm [simplified] by fast
qed
qed
@@ -543,9 +541,10 @@
proof -
interpret G: abelian_group G by fact
interpret H: abelian_group H by fact
- show ?thesis apply (intro abelian_group_hom.intro abelian_group_hom_axioms.intro)
- apply fact
- apply fact
+ show ?thesis
+ apply (intro abelian_group_hom.intro abelian_group_hom_axioms.intro)
+ apply fact
+ apply fact
apply (rule a_group_hom)
done
qed
--- a/src/HOL/Tools/inductive_set.ML Mon Nov 07 14:16:01 2011 +0100
+++ b/src/HOL/Tools/inductive_set.ML Mon Nov 07 17:24:57 2011 +0100
@@ -22,6 +22,8 @@
(binding * string option * mixfix) list ->
(Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list ->
bool -> local_theory -> Inductive.inductive_result * local_theory
+ val mono_add: attribute
+ val mono_del: attribute
val codegen_preproc: theory -> thm list -> thm list
val setup: theory -> theory
end;
@@ -536,13 +538,12 @@
val add_inductive_i = Inductive.gen_add_inductive_i add_ind_set_def;
val add_inductive = Inductive.gen_add_inductive add_ind_set_def;
-fun mono_att att = (* FIXME really mixed_attribute!? *)
- Thm.mixed_attribute (fn (context, thm) =>
- let val thm' = to_pred [] context thm
- in (Thm.attribute_declaration att thm' context, thm') end);
+fun mono_att att =
+ Thm.declaration_attribute (fn thm => fn context =>
+ Thm.attribute_declaration att (to_pred [] context thm) context);
-val mono_add_att = mono_att Inductive.mono_add;
-val mono_del_att = mono_att Inductive.mono_del;
+val mono_add = mono_att Inductive.mono_add;
+val mono_del = mono_att Inductive.mono_del;
(** package setup **)
@@ -556,7 +557,7 @@
"convert rule to set notation" #>
Attrib.setup @{binding to_pred} (Attrib.thms >> to_pred_att)
"convert rule to predicate notation" #>
- Attrib.setup @{binding mono_set} (Attrib.add_del mono_add_att mono_del_att)
+ Attrib.setup @{binding mono_set} (Attrib.add_del mono_add mono_del)
"declaration of monotonicity rule for set operators" #>
Simplifier.map_simpset_global (fn ss => ss addsimprocs [collect_mem_simproc]);
--- a/src/Pure/Isar/attrib.ML Mon Nov 07 14:16:01 2011 +0100
+++ b/src/Pure/Isar/attrib.ML Mon Nov 07 17:24:57 2011 +0100
@@ -16,12 +16,12 @@
val defined: theory -> string -> bool
val attribute: theory -> src -> attribute
val attribute_i: theory -> src -> attribute
- val map_specs: ('a -> 'att) ->
+ val map_specs: ('a list -> 'att list) ->
(('c * 'a list) * 'b) list -> (('c * 'att list) * 'b) list
- val map_facts: ('a -> 'att) ->
+ val map_facts: ('a list -> 'att list) ->
(('c * 'a list) * ('d * 'a list) list) list ->
(('c * 'att list) * ('d * 'att list) list) list
- val map_facts_refs: ('a -> 'att) -> ('b -> 'fact) ->
+ val map_facts_refs: ('a list -> 'att list) -> ('b -> 'fact) ->
(('c * 'a list) * ('b * 'a list) list) list ->
(('c * 'att list) * ('fact * 'att list) list) list
val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
@@ -127,9 +127,9 @@
(* attributed declarations *)
-fun map_specs f = map (apfst (apsnd (map f)));
+fun map_specs f = map (apfst (apsnd f));
-fun map_facts f = map (apfst (apsnd (map f)) o apsnd (map (apsnd (map f))));
+fun map_facts f = map (apfst (apsnd f) o apsnd (map (apsnd f)));
fun map_facts_refs f g = map_facts f #> map (apsnd (map (apfst g)));
@@ -137,7 +137,7 @@
fun eval_thms ctxt srcs = ctxt
|> Proof_Context.note_thmss ""
- (map_facts_refs (attribute (Proof_Context.theory_of ctxt)) (Proof_Context.get_fact ctxt)
+ (map_facts_refs (map (attribute (Proof_Context.theory_of ctxt))) (Proof_Context.get_fact ctxt)
[((Binding.empty, []), srcs)])
|> fst |> maps snd;
--- a/src/Pure/Isar/element.ML Mon Nov 07 14:16:01 2011 +0100
+++ b/src/Pure/Isar/element.ML Mon Nov 07 17:24:57 2011 +0100
@@ -481,7 +481,8 @@
fun generic_note_thmss kind facts context =
let
- val facts' = Attrib.map_facts (Attrib.attribute_i (Context.theory_of context)) facts;
+ val facts' =
+ Attrib.map_facts (map (Attrib.attribute_i (Context.theory_of context))) facts;
in
context |> Context.mapping_result
(Global_Theory.note_thmss kind facts')
@@ -492,14 +493,16 @@
| init (Constrains _) = I
| init (Assumes asms) = Context.map_proof (fn ctxt =>
let
- val asms' = Attrib.map_specs (Attrib.attribute_i (Proof_Context.theory_of ctxt)) asms;
+ val asms' =
+ Attrib.map_specs (map (Attrib.attribute_i (Proof_Context.theory_of ctxt))) asms;
val (_, ctxt') = ctxt
|> fold Variable.auto_fixes (maps (map #1 o #2) asms')
|> Proof_Context.add_assms_i Assumption.assume_export asms';
in ctxt' end)
| init (Defines defs) = Context.map_proof (fn ctxt =>
let
- val defs' = Attrib.map_specs (Attrib.attribute_i (Proof_Context.theory_of ctxt)) defs;
+ val defs' =
+ Attrib.map_specs (map (Attrib.attribute_i (Proof_Context.theory_of ctxt))) defs;
val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
let val ((c, _), t') = Local_Defs.cert_def ctxt t (* FIXME adapt ps? *)
in (t', ((Thm.def_binding_optional (Binding.name c) name, atts), [(t', ps)])) end);
--- a/src/Pure/Isar/generic_target.ML Mon Nov 07 14:16:01 2011 +0100
+++ b/src/Pure/Isar/generic_target.ML Mon Nov 07 17:24:57 2011 +0100
@@ -156,7 +156,7 @@
in
lthy
|> target_notes kind global_facts local_facts
- |> Proof_Context.note_thmss kind (Attrib.map_facts (Attrib.attribute_i thy) local_facts)
+ |> Proof_Context.note_thmss kind (Attrib.map_facts (map (Attrib.attribute_i thy)) local_facts)
end;
@@ -212,7 +212,7 @@
fun theory_notes kind global_facts lthy =
let
val thy = Proof_Context.theory_of lthy;
- val global_facts' = Attrib.map_facts (Attrib.attribute_i thy) global_facts;
+ val global_facts' = Attrib.map_facts (map (Attrib.attribute_i thy)) global_facts;
in
lthy
|> Local_Theory.background_theory (Global_Theory.note_thmss kind global_facts' #> snd)
--- a/src/Pure/Isar/locale.ML Mon Nov 07 14:16:01 2011 +0100
+++ b/src/Pure/Isar/locale.ML Mon Nov 07 17:24:57 2011 +0100
@@ -562,8 +562,9 @@
(* Registrations *)
(fn thy => fold_rev (fn (_, morph) =>
let
- val args'' = snd args' |> Element.facts_map (Element.transform_ctxt morph) |>
- Attrib.map_facts (Attrib.attribute_i thy)
+ val args'' = snd args'
+ |> Element.facts_map (Element.transform_ctxt morph)
+ |> Attrib.map_facts (map (Attrib.attribute_i thy));
in Global_Theory.note_thmss kind args'' #> snd end)
(registrations_of (Context.Theory thy) loc) thy))
in ctxt'' end;
--- a/src/Pure/Isar/named_target.ML Mon Nov 07 14:16:01 2011 +0100
+++ b/src/Pure/Isar/named_target.ML Mon Nov 07 17:24:57 2011 +0100
@@ -117,7 +117,7 @@
fun locale_notes locale kind global_facts local_facts lthy =
let
- val global_facts' = Attrib.map_facts (K (Thm.mixed_attribute I)) global_facts;
+ val global_facts' = Attrib.map_facts (K []) global_facts;
val local_facts' = Element.facts_map
(Element.transform_ctxt (Local_Theory.target_morphism lthy)) local_facts;
in
--- a/src/Pure/Isar/obtain.ML Mon Nov 07 14:16:01 2011 +0100
+++ b/src/Pure/Isar/obtain.ML Mon Nov 07 17:24:57 2011 +0100
@@ -126,7 +126,7 @@
val (proppss, asms_ctxt) = prep_propp (map snd raw_asms) fix_ctxt;
val ((_, bind_ctxt), _) = Proof_Context.bind_propp_i proppss asms_ctxt;
val asm_props = maps (map fst) proppss;
- val asms = map fst (Attrib.map_specs (prep_att thy) raw_asms) ~~ proppss;
+ val asms = map fst (Attrib.map_specs (map (prep_att thy)) raw_asms) ~~ proppss;
(*obtain parms*)
val (Ts, parms_ctxt) = fold_map Proof_Context.inferred_param xs' asms_ctxt;
--- a/src/Pure/Isar/proof.ML Mon Nov 07 14:16:01 2011 +0100
+++ b/src/Pure/Isar/proof.ML Mon Nov 07 17:24:57 2011 +0100
@@ -593,7 +593,7 @@
fun gen_assume asm prep_att exp args state =
state
|> assert_forward
- |> map_context_result (asm exp (Attrib.map_specs (prep_att (theory_of state)) args))
+ |> map_context_result (asm exp (Attrib.map_specs (map (prep_att (theory_of state))) args))
|> these_factss [] |> #2;
in
@@ -665,7 +665,9 @@
state
|> assert_forward
|> map_context_result (Proof_Context.note_thmss ""
- (Attrib.map_facts_refs (prep_atts (theory_of state)) (prep_fact (context_of state)) args))
+ (Attrib.map_facts_refs
+ (map (prep_atts (theory_of state)))
+ (prep_fact (context_of state)) args))
|> these_factss (more_facts state)
||> opt_chain
|> opt_result;
@@ -690,12 +692,12 @@
local
-fun gen_using f g prep_atts prep_fact args state =
+fun gen_using f g prep_att prep_fact args state =
state
|> assert_backward
|> map_context_result
(Proof_Context.note_thmss ""
- (Attrib.map_facts_refs (prep_atts (theory_of state)) (prep_fact (context_of state))
+ (Attrib.map_facts_refs (map (prep_att (theory_of state))) (prep_fact (context_of state))
(no_binding args)))
|> (fn (named_facts, state') =>
state' |> map_goal I (fn (statement, _, using, goal, before_qed, after_qed) =>
@@ -916,7 +918,7 @@
let
val thy = theory_of state;
val ((names, attss), propp) =
- Attrib.map_specs (prep_att thy) stmt |> split_list |>> split_list;
+ Attrib.map_specs (map (prep_att thy)) stmt |> split_list |>> split_list;
fun after_qed' results =
local_results ((names ~~ attss) ~~ results)
--- a/src/Pure/Isar/specification.ML Mon Nov 07 14:16:01 2011 +0100
+++ b/src/Pure/Isar/specification.ML Mon Nov 07 17:24:57 2011 +0100
@@ -307,7 +307,7 @@
let
val (propp, elems_ctxt) = prep_stmt elems (map snd shows) ctxt;
val prems = Assumption.local_prems_of elems_ctxt ctxt;
- val stmt = Attrib.map_specs prep_att (map fst shows ~~ propp);
+ val stmt = Attrib.map_specs (map prep_att) (map fst shows ~~ propp);
val goal_ctxt = (fold o fold) (Variable.auto_fixes o fst) propp elems_ctxt;
in ((prems, stmt, NONE), goal_ctxt) end
| Element.Obtains obtains =>
--- a/src/Pure/Syntax/syntax_trans.ML Mon Nov 07 14:16:01 2011 +0100
+++ b/src/Pure/Syntax/syntax_trans.ML Mon Nov 07 17:24:57 2011 +0100
@@ -231,48 +231,24 @@
(* indexed syntax *)
+fun indexdefault_ast_tr [] =
+ Ast.Appl [Ast.Constant "_index",
+ Ast.Appl [Ast.Constant "_struct", Ast.Constant "_indexdefault"]]
+ | indexdefault_ast_tr asts = raise Ast.AST ("indexdefault_ast_tr", asts);
+
+fun indexvar_ast_tr [] = Ast.Appl [Ast.Constant "_index", Ast.Variable "some_index"]
+ | indexvar_ast_tr asts = raise Ast.AST ("indexvar_ast_tr", asts);
+
fun struct_ast_tr [Ast.Appl [Ast.Constant "_index", ast]] = ast
| struct_ast_tr asts = Ast.mk_appl (Ast.Constant "_struct") asts;
-fun index_ast_tr ast =
- Ast.mk_appl (Ast.Constant "_index") [Ast.mk_appl (Ast.Constant "_struct") [ast]];
-
-fun indexdefault_ast_tr [] = index_ast_tr (Ast.Constant "_indexdefault")
- | indexdefault_ast_tr asts = raise Ast.AST ("indexdefault_ast_tr", asts);
-
-fun indexnum_ast_tr [ast] = index_ast_tr (Ast.mk_appl (Ast.Constant "_indexnum") [ast])
- | indexnum_ast_tr asts = raise Ast.AST ("indexnum_ast_tr", asts);
-
-fun indexvar_ast_tr [] = Ast.mk_appl (Ast.Constant "_index") [Ast.Variable "some_index"]
- | indexvar_ast_tr asts = raise Ast.AST ("indexvar_ast_tr", asts);
-
fun index_tr [t] = t
| index_tr ts = raise TERM ("index_tr", ts);
-
-(* implicit structures *)
-
-fun the_struct structs i =
- if 1 <= i andalso i <= length structs then nth structs (i - 1)
- else error ("Illegal reference to implicit structure #" ^ string_of_int i);
+fun the_struct [] = error "Illegal reference to implicit structure"
+ | the_struct (x :: _) = x;
-fun legacy_struct structs i =
- let
- val x = the_struct structs i;
- val _ =
- legacy_feature
- ("Old-style numbered structure index " ^ quote ("\\<^sub>" ^ string_of_int i) ^
- Position.str_of (Position.thread_data ()) ^
- " -- use " ^ quote ("\\<^bsub>" ^ x ^ "\\<^esub>") ^ " instead" ^
- (if i = 1 then " (may be omitted)" else ""))
- in x end;
-
-fun struct_tr structs [Const ("_indexdefault", _)] = Syntax.free (the_struct structs 1)
- | struct_tr structs [Const ("_index1", _)] = Syntax.free (legacy_struct structs 1)
- | struct_tr structs [t as (Const ("_indexnum", _) $ Const (s, _))] =
- (case Lexicon.read_nat s of
- SOME i => Syntax.free (legacy_struct structs i)
- | NONE => raise TERM ("struct_tr", [t]))
+fun struct_tr structs [Const ("_indexdefault", _)] = Syntax.free (the_struct structs)
| struct_tr _ ts = raise TERM ("struct_tr", ts);
@@ -517,17 +493,9 @@
fun index_ast_tr' [Ast.Appl [Ast.Constant "_struct", ast]] = ast
| index_ast_tr' _ = raise Match;
-
-(* implicit structures *)
-
-fun the_struct' structs s =
- [(case Lexicon.read_nat s of
- SOME i => Ast.Variable (the_struct structs i handle ERROR _ => raise Match)
- | NONE => raise Match)] |> Ast.mk_appl (Ast.Constant "_free");
-
-fun struct_ast_tr' structs [Ast.Constant "_indexdefault"] = the_struct' structs "1"
- | struct_ast_tr' structs [Ast.Appl [Ast.Constant "_indexnum", Ast.Constant s]] =
- the_struct' structs s
+fun struct_ast_tr' structs [Ast.Constant "_indexdefault"] =
+ Ast.Appl [Ast.Constant "_free",
+ Ast.Variable (the_struct structs handle ERROR _ => raise Match)]
| struct_ast_tr' _ _ = raise Match;
@@ -547,7 +515,6 @@
("_idtypdummy", idtypdummy_ast_tr),
("_bigimpl", bigimpl_ast_tr),
("_indexdefault", indexdefault_ast_tr),
- ("_indexnum", indexnum_ast_tr),
("_indexvar", indexvar_ast_tr),
("_struct", struct_ast_tr)],
[("_abs", abs_tr),
--- a/src/Pure/System/Java_Ext_Dirs.java Mon Nov 07 14:16:01 2011 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
-/* Title: Pure/System/Java_Ext_Dirs.java
- Author: Makarius
-
-Augment Java extension directories.
-*/
-
-package isabelle;
-
-public class Java_Ext_Dirs
-{
- public static void main(String [] args) {
- StringBuilder s = new StringBuilder();
- int i;
- for (i = 0; i < args.length; i++) {
- s.append(args[i]);
- s.append(System.getProperty("path.separator"));
- }
- s.append(System.getProperty("java.ext.dirs"));
- System.out.println(s.toString());
- }
-}
-
--- a/src/Pure/pure_thy.ML Mon Nov 07 14:16:01 2011 +0100
+++ b/src/Pure/pure_thy.ML Mon Nov 07 17:24:57 2011 +0100
@@ -127,8 +127,6 @@
("_strip_positions", typ "'a", NoSyn),
("_constify", typ "num => num_const", Delimfix "_"),
("_constify", typ "float_token => float_const", Delimfix "_"),
- ("_index1", typ "index", Delimfix "\\<^sub>1"),
- ("_indexnum", typ "num_const => index", Delimfix "\\<^sub>_"),
("_index", typ "logic => index", Delimfix "(00\\<^bsub>_\\<^esub>)"),
("_indexdefault", typ "index", Delimfix ""),
("_indexvar", typ "index", Delimfix "'\\<index>"),
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/JVM/Java_Ext_Dirs.java Mon Nov 07 17:24:57 2011 +0100
@@ -0,0 +1,22 @@
+/* Title: Pure/System/Java_Ext_Dirs.java
+ Author: Makarius
+
+Augment Java extension directories.
+*/
+
+package isabelle;
+
+public class Java_Ext_Dirs
+{
+ public static void main(String [] args) {
+ StringBuilder s = new StringBuilder();
+ int i;
+ for (i = 0; i < args.length; i++) {
+ s.append(args[i]);
+ s.append(System.getProperty("path.separator"));
+ }
+ s.append(System.getProperty("java.ext.dirs"));
+ System.out.println(s.toString());
+ }
+}
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/JVM/build Mon Nov 07 17:24:57 2011 +0100
@@ -0,0 +1,31 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# Offline build script for JVM tools.
+
+## diagnostics
+
+function fail()
+{
+ echo "$1" >&2
+ exit 2
+}
+
+
+## build
+
+cd "$(dirname "$0")"
+
+SOURCE="Java_Ext_Dirs.java"
+TARGET="java_ext_dirs.jar"
+
+BUILD="build_dir$$"
+TMP_JAR="java_ext_dirs$$.jar"
+
+rm -rf "$BUILD" && mkdir "$BUILD"
+javac -source 1.4 -target 1.4 -d "$BUILD" "$SOURCE" || fail "Failed to compile sources"
+jar cf "$TMP_JAR" -C "$BUILD" . || fail "Failed to produce \"$TMP_JAR\""
+mv "$TMP_JAR" "$TARGET"
+rm -rf "$BUILD"
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/JVM/java_ext_dirs Mon Nov 07 17:24:57 2011 +0100
@@ -0,0 +1,23 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# Augment Java extension directories.
+
+## diagnostics
+
+function fail()
+{
+ echo "$1" >&2
+ exit 2
+}
+
+[ -n "$ISABELLE_HOME" ] || fail "Missing Isabelle settings environment"
+
+
+## main
+
+JAVA_EXE="${THIS_JAVA:-$ISABELLE_JAVA}"
+exec "$JAVA_EXE" -classpath "$(jvmpath "$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs.jar")" \
+ isabelle.Java_Ext_Dirs "$(jvmpath "$ISABELLE_HOME/lib/classes/ext")"
+
Binary file src/Tools/JVM/java_ext_dirs.jar has changed