# HG changeset patch # User wenzelm # Date 1378577558 -7200 # Node ID 8adcf1f0042d309da09a3a55d2b2f1419c676c6b # Parent 6301ed01e34dbe755007be20052b3f5178218687# Parent 19e7d50446178763636a681607f538a832d68167 merged diff -r 6301ed01e34d -r 8adcf1f0042d Admin/MacOS/App3/Info.plist --- a/Admin/MacOS/App3/Info.plist Fri Sep 06 20:59:36 2013 +0200 +++ b/Admin/MacOS/App3/Info.plist Sat Sep 07 20:12:38 2013 +0200 @@ -34,7 +34,7 @@ isabelle.Main JVMOptions --Dapple.laf.useScreenMenuBar=true +-Dapple.laf.useScreenMenuBar=true -Xms128m -Xmx1024m -Xss2m -Dactors.corePoolSize=4 -Dactors.enableForkJoin=false -Disabelle.home=$APP_ROOT/Contents/Resources/{ISABELLE_NAME} JVMArguments diff -r 6301ed01e34d -r 8adcf1f0042d Admin/Windows/launch4j/isabelle.xml --- a/Admin/Windows/launch4j/isabelle.xml Fri Sep 06 20:59:36 2013 +0200 +++ b/Admin/Windows/launch4j/isabelle.xml Sat Sep 07 20:12:38 2013 +0200 @@ -16,15 +16,19 @@ isabelle.Main %EXEDIR%\lib\classes\ext\Pure.jar + %EXEDIR%\lib\classes\ext\scala-compiler.jar %EXEDIR%\lib\classes\ext\scala-library.jar %EXEDIR%\lib\classes\ext\scala-swing.jar + %EXEDIR%\lib\classes\ext\scala-actors.jar + %EXEDIR%\lib\classes\ext\scala-reflect.jar + %EXEDIR%\src\Tools\jEdit\dist\jedit.jar %EXEDIR%\contrib\jdk\x86-cygwin jdkOnly - -Disabelle.home="%EXEDIR%" + -Dfile.encoding=UTF-8 -server -Xms128m -Xmx1024m -Xss2m -Dactors.corePoolSize=4 -Dactors.enableForkJoin=false -Disabelle.home="%EXEDIR%" isabelle.bmp diff -r 6301ed01e34d -r 8adcf1f0042d Admin/build --- a/Admin/build Fri Sep 06 20:59:36 2013 +0200 +++ b/Admin/build Sat Sep 07 20:12:38 2013 +0200 @@ -74,6 +74,10 @@ ## main +#workaround for scalac +function stty() { :; } +export -f stty + for MODULE in $MODULES do case $MODULE in diff -r 6301ed01e34d -r 8adcf1f0042d Admin/components/bundled-windows --- a/Admin/components/bundled-windows Fri Sep 06 20:59:36 2013 +0200 +++ b/Admin/components/bundled-windows Sat Sep 07 20:12:38 2013 +0200 @@ -1,3 +1,3 @@ #additional components to be bundled for release cygwin-20130117 -windows_app-20130905 +windows_app-20130906 diff -r 6301ed01e34d -r 8adcf1f0042d Admin/components/components.sha1 --- a/Admin/components/components.sha1 Fri Sep 06 20:59:36 2013 +0200 +++ b/Admin/components/components.sha1 Sat Sep 07 20:12:38 2013 +0200 @@ -55,6 +55,7 @@ 869ea6d8ea35c8ba68d7fcb028f16b2b7064c5fd vampire-1.0.tar.gz 81d21dfd0ea5c58f375301f5166be9dbf8921a7a windows_app-20130716.tar.gz fe15e1079cf5ad86f3cbab4553722a0d20002d11 windows_app-20130905.tar.gz +e6a43b7b3b21295853bd2a63b27ea20bd6102f5f windows_app-20130906.tar.gz 2ae13aa17d0dc95ce254a52f1dba10929763a10d xz-java-1.2.tar.gz 4530a1aa6f4498ee3d78d6000fa71a3f63bd077f yices-1.0.28.tar.gz 12ae71acde43bd7bed1e005c43034b208c0cba4c z3-3.2.tar.gz diff -r 6301ed01e34d -r 8adcf1f0042d Admin/lib/Tools/makedist_bundle --- a/Admin/lib/Tools/makedist_bundle Fri Sep 06 20:59:36 2013 +0200 +++ b/Admin/lib/Tools/makedist_bundle Sat Sep 07 20:12:38 2013 +0200 @@ -126,6 +126,15 @@ case "$PLATFORM_FAMILY" in linux) purge_contrib '-name "x86*-darwin" -o -name "x86*-cygwin" -o -name "x86*-windows"' + cat > "$ISABELLE_TARGET/$ISABELLE_NAME" < "$APP/Contents/Info.plist" - for NAME in Pure.jar scala-library.jar scala-swing.jar + for NAME in Pure.jar scala-compiler.jar scala-library.jar scala-swing.jar scala-actors.jar scala-reflect.jar do ln -sf "../Resources/${ISABELLE_NAME}/lib/classes/ext/$NAME" "$APP/Contents/Java" done + ln -sf "../Resources/${ISABELLE_NAME}/src/Tools/jEdit/dist/jedit.jar" "$APP/Contents/Java" cp -R "$APP_TEMPLATE/Resources/." "$APP/Contents/Resources/." cp "$APP_TEMPLATE/../isabelle.icns" "$APP/Contents/Resources/." diff -r 6301ed01e34d -r 8adcf1f0042d Isabelle --- a/Isabelle Fri Sep 06 20:59:36 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,8 +0,0 @@ -#!/usr/bin/env bash -# -# Author: Makarius -# -# Default Isabelle application wrapper. - -exec "$(dirname "$0")"/bin/isabelle jedit -s -- "$@" - diff -r 6301ed01e34d -r 8adcf1f0042d src/HOL/Multivariate_Analysis/Integration.thy --- a/src/HOL/Multivariate_Analysis/Integration.thy Fri Sep 06 20:59:36 2013 +0200 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Sat Sep 07 20:12:38 2013 +0200 @@ -3125,131 +3125,284 @@ subsection {* Cauchy-type criterion for integrability. *} (* XXXXXXX *) -lemma integrable_cauchy: fixes f::"'n::ordered_euclidean_space \ 'a::{real_normed_vector,complete_space}" +lemma integrable_cauchy: + fixes f :: "'n::ordered_euclidean_space \ 'a::{real_normed_vector,complete_space}" shows "f integrable_on {a..b} \ - (\e>0.\d. gauge d \ (\p1 p2. p1 tagged_division_of {a..b} \ d fine p1 \ - p2 tagged_division_of {a..b} \ d fine p2 - \ norm(setsum (\(x,k). content k *\<^sub>R f x) p1 - - setsum (\(x,k). content k *\<^sub>R f x) p2) < e))" (is "?l = (\e>0. \d. ?P e d)") -proof assume ?l + (\e>0.\d. gauge d \ + (\p1 p2. p1 tagged_division_of {a..b} \ d fine p1 \ + p2 tagged_division_of {a..b} \ d fine p2 \ + norm (setsum (\(x,k). content k *\<^sub>R f x) p1 - + setsum (\(x,k). content k *\<^sub>R f x) p2) < e))" + (is "?l = (\e>0. \d. ?P e d)") +proof + assume ?l then guess y unfolding integrable_on_def has_integral .. note y=this - show "\e>0. \d. ?P e d" proof(rule,rule) case goal1 hence "e/2 > 0" by auto + show "\e>0. \d. ?P e d" + proof (rule, rule) + case goal1 + then have "e/2 > 0" by auto then guess d apply- apply(drule y[rule_format]) by(erule exE,erule conjE) note d=this[rule_format] - show ?case apply(rule_tac x=d in exI,rule,rule d) apply(rule,rule,rule,(erule conjE)+) - proof- fix p1 p2 assume as:"p1 tagged_division_of {a..b}" "d fine p1" "p2 tagged_division_of {a..b}" "d fine p2" + show ?case + apply (rule_tac x=d in exI) + apply rule + apply (rule d) + apply rule + apply rule + apply rule + apply (erule conjE)+ + proof - + fix p1 p2 + assume as: "p1 tagged_division_of {a..b}" "d fine p1" + "p2 tagged_division_of {a..b}" "d fine p2" show "norm ((\(x, k)\p1. content k *\<^sub>R f x) - (\(x, k)\p2. content k *\<^sub>R f x)) < e" - apply(rule dist_triangle_half_l[where y=y,unfolded dist_norm]) + apply (rule dist_triangle_half_l[where y=y,unfolded dist_norm]) using d(2)[OF conjI[OF as(1-2)]] d(2)[OF conjI[OF as(3-4)]] . - qed qed -next assume "\e>0. \d. ?P e d" hence "\n::nat. \d. ?P (inverse(real (n + 1))) d" by auto + qed + qed +next + assume "\e>0. \d. ?P e d" + then have "\n::nat. \d. ?P (inverse(real (n + 1))) d" + by auto from choice[OF this] guess d .. note d=conjunctD2[OF this[rule_format],rule_format] - have "\n. gauge (\x. \{d i x |i. i \ {0..n}})" apply(rule gauge_inters) using d(1) by auto - hence "\n. \p. p tagged_division_of {a..b} \ (\x. \{d i x |i. i \ {0..n}}) fine p" apply- - proof case goal1 from this[of n] show ?case apply(drule_tac fine_division_exists) by auto qed + have "\n. gauge (\x. \{d i x |i. i \ {0..n}})" + apply (rule gauge_inters) + using d(1) + apply auto + done + then have "\n. \p. p tagged_division_of {a..b} \ (\x. \{d i x |i. i \ {0..n}}) fine p" + apply - + proof + case goal1 + from this[of n] + show ?case + apply (drule_tac fine_division_exists) + apply auto + done + qed from choice[OF this] guess p .. note p = conjunctD2[OF this[rule_format]] - have dp:"\i n. i\n \ d i fine p n" using p(2) unfolding fine_inters by auto + have dp: "\i n. i\n \ d i fine p n" + using p(2) unfolding fine_inters by auto have "Cauchy (\n. setsum (\(x,k). content k *\<^sub>R (f x)) (p n))" - proof(rule CauchyI) case goal1 then guess N unfolding real_arch_inv[of e] .. note N=this - show ?case apply(rule_tac x=N in exI) - proof(rule,rule,rule,rule) fix m n assume mn:"N \ m" "N \ n" have *:"N = (N - 1) + 1" using N by auto + proof (rule CauchyI) + case goal1 + then guess N unfolding real_arch_inv[of e] .. note N=this + show ?case + apply (rule_tac x=N in exI) + proof (rule, rule, rule, rule) + fix m n + assume mn: "N \ m" "N \ n" + have *: "N = (N - 1) + 1" using N by auto show "norm ((\(x, k)\p m. content k *\<^sub>R f x) - (\(x, k)\p n. content k *\<^sub>R f x)) < e" - apply(rule less_trans[OF _ N[THEN conjunct2,THEN conjunct2]]) apply(subst *) apply(rule d(2)) - using dp p(1) using mn by auto - qed qed + apply (rule less_trans[OF _ N[THEN conjunct2,THEN conjunct2]]) + apply(subst *) + apply(rule d(2)) + using dp p(1) + using mn + apply auto + done + qed + qed then guess y unfolding convergent_eq_cauchy[symmetric] .. note y=this[THEN LIMSEQ_D] - show ?l unfolding integrable_on_def has_integral apply(rule_tac x=y in exI) - proof(rule,rule) fix e::real assume "e>0" hence *:"e/2 > 0" by auto - then guess N1 unfolding real_arch_inv[of "e/2"] .. note N1=this hence N1':"N1 = N1 - 1 + 1" by auto + show ?l + unfolding integrable_on_def has_integral + apply (rule_tac x=y in exI) + proof (rule, rule) + fix e :: real + assume "e>0" + then have *:"e/2 > 0" by auto + then guess N1 unfolding real_arch_inv[of "e/2"] .. note N1=this + then have N1': "N1 = N1 - 1 + 1" + by auto guess N2 using y[OF *] .. note N2=this - show "\d. gauge d \ (\p. p tagged_division_of {a..b} \ d fine p \ norm ((\(x, k)\p. content k *\<^sub>R f x) - y) < e)" - apply(rule_tac x="d (N1 + N2)" in exI) apply rule defer - proof(rule,rule,erule conjE) show "gauge (d (N1 + N2))" using d by auto - fix q assume as:"q tagged_division_of {a..b}" "d (N1 + N2) fine q" - have *:"inverse (real (N1 + N2 + 1)) < e / 2" apply(rule less_trans) using N1 by auto - show "norm ((\(x, k)\q. content k *\<^sub>R f x) - y) < e" apply(rule norm_triangle_half_r) - apply(rule less_trans[OF _ *]) apply(subst N1', rule d(2)[of "p (N1+N2)"]) defer + show "\d. gauge d \ + (\p. p tagged_division_of {a..b} \ d fine p \ norm ((\(x, k)\p. content k *\<^sub>R f x) - y) < e)" + apply (rule_tac x="d (N1 + N2)" in exI) + apply rule + defer + proof (rule, rule, erule conjE) + show "gauge (d (N1 + N2))" + using d by auto + fix q + assume as: "q tagged_division_of {a..b}" "d (N1 + N2) fine q" + have *: "inverse (real (N1 + N2 + 1)) < e / 2" + apply (rule less_trans) + using N1 + apply auto + done + show "norm ((\(x, k)\q. content k *\<^sub>R f x) - y) < e" + apply (rule norm_triangle_half_r) + apply (rule less_trans[OF _ *]) + apply (subst N1', rule d(2)[of "p (N1+N2)"]) + defer using N2[rule_format,of "N1+N2"] - using as dp[of "N1 - 1 + 1 + N2" "N1 + N2"] using p(1)[of "N1 + N2"] using N1 by auto qed qed qed + using as dp[of "N1 - 1 + 1 + N2" "N1 + N2"] + using p(1)[of "N1 + N2"] + using N1 + apply auto + done + qed + qed +qed + subsection {* Additivity of integral on abutting intervals. *} lemma interval_split: - fixes a::"'a::ordered_euclidean_space" assumes "k \ Basis" + fixes a :: "'a::ordered_euclidean_space" + assumes "k \ Basis" shows "{a..b} \ {x. x\k \ c} = {a .. (\i\Basis. (if i = k then min (b\k) c else b\i) *\<^sub>R i)}" "{a..b} \ {x. x\k \ c} = {(\i\Basis. (if i = k then max (a\k) c else a\i) *\<^sub>R i) .. b}" - apply(rule_tac[!] set_eqI) unfolding Int_iff mem_interval mem_Collect_eq using assms - by auto - -lemma content_split: fixes a::"'a::ordered_euclidean_space" assumes "k\Basis" shows - "content {a..b} = content({a..b} \ {x. x\k \ c}) + content({a..b} \ {x. x\k >= c})" + apply (rule_tac[!] set_eqI) + unfolding Int_iff mem_interval mem_Collect_eq + using assms + apply auto + done + +lemma content_split: + fixes a :: "'a::ordered_euclidean_space" + assumes "k \ Basis" + shows "content {a..b} = content({a..b} \ {x. x\k \ c}) + content({a..b} \ {x. x\k \ c})" proof cases note simps = interval_split[OF assms] content_closed_interval_cases eucl_le[where 'a='a] - have *:"Basis = insert k (Basis - {k})" "\x. finite (Basis-{x})" "\x. x\Basis-{x}" + have *: "Basis = insert k (Basis - {k})" "\x. finite (Basis-{x})" "\x. x\Basis-{x}" using assms by auto - have *:"\X Y Z. (\i\Basis. Z i (if i = k then X else Y i)) = Z k X * (\i\Basis-{k}. Z i (Y i))" + have *: "\X Y Z. (\i\Basis. Z i (if i = k then X else Y i)) = Z k X * (\i\Basis-{k}. Z i (Y i))" "(\i\Basis. b\i - a\i) = (\i\Basis-{k}. b\i - a\i) * (b\k - a\k)" - apply(subst *(1)) defer apply(subst *(1)) unfolding setprod_insert[OF *(2-)] by auto - assume as:"a\b" moreover have "\x. min (b \ k) c = max (a \ k) c - \ x* (b\k - a\k) = x*(max (a \ k) c - a \ k) + x*(b \ k - max (a \ k) c)" - by (auto simp add:field_simps) - moreover have **:"(\i\Basis. ((\i\Basis. (if i = k then min (b \ k) c else b \ i) *\<^sub>R i) \ i - a \ i)) = + apply (subst *(1)) + defer + apply (subst *(1)) + unfolding setprod_insert[OF *(2-)] + apply auto + done + assume as: "a \ b" + moreover + have "\x. min (b \ k) c = max (a \ k) c \ + x * (b\k - a\k) = x * (max (a \ k) c - a \ k) + x * (b \ k - max (a \ k) c)" + by (auto simp add: field_simps) + moreover + have **: "(\i\Basis. ((\i\Basis. (if i = k then min (b \ k) c else b \ i) *\<^sub>R i) \ i - a \ i)) = (\i\Basis. (if i = k then min (b \ k) c else b \ i) - a \ i)" "(\i\Basis. b \ i - ((\i\Basis. (if i = k then max (a \ k) c else a \ i) *\<^sub>R i) \ i)) = (\i\Basis. b \ i - (if i = k then max (a \ k) c else a \ i))" by (auto intro!: setprod_cong) have "\ a \ k \ c \ \ c \ b \ k \ False" - unfolding not_le using as[unfolded eucl_le[where 'a='a],rule_format,of k] assms by auto - ultimately show ?thesis using assms unfolding simps ** - unfolding *(1)[of "\i x. b\i - x"] *(1)[of "\i x. x - a\i"] unfolding *(2) + unfolding not_le + using as[unfolded eucl_le[where 'a='a],rule_format,of k] assms + by auto + ultimately show ?thesis + using assms + unfolding simps ** + unfolding *(1)[of "\i x. b\i - x"] *(1)[of "\i x. x - a\i"] + unfolding *(2) by auto next - assume "\ a \ b" then have "{a .. b} = {}" + assume "\ a \ b" + then have "{a .. b} = {}" unfolding interval_eq_empty by (auto simp: eucl_le[where 'a='a] not_le) - then show ?thesis by auto + then show ?thesis + by auto qed -lemma division_split_left_inj: fixes type::"'a::ordered_euclidean_space" - assumes "d division_of i" "k1 \ d" "k2 \ d" "k1 \ k2" - "k1 \ {x::'a. x\k \ c} = k2 \ {x. x\k \ c}"and k:"k\Basis" +lemma division_split_left_inj: + fixes type :: "'a::ordered_euclidean_space" + assumes "d division_of i" + and "k1 \ d" + and "k2 \ d" + and "k1 \ k2" + and "k1 \ {x::'a. x\k \ c} = k2 \ {x. x\k \ c}" + and k: "k\Basis" shows "content(k1 \ {x. x\k \ c}) = 0" -proof- note d=division_ofD[OF assms(1)] - have *:"\a b::'a. \ c. (content({a..b} \ {x. x\k \ c}) = 0 \ interior({a..b} \ {x. x\k \ c}) = {})" +proof - + note d=division_ofD[OF assms(1)] + have *: "\a b::'a. \ c. (content({a..b} \ {x. x\k \ c}) = 0 \ interior({a..b} \ {x. x\k \ c}) = {})" unfolding interval_split[OF k] content_eq_0_interior by auto guess u1 v1 using d(4)[OF assms(2)] apply-by(erule exE)+ note uv1=this guess u2 v2 using d(4)[OF assms(3)] apply-by(erule exE)+ note uv2=this - have **:"\s t u. s \ t = {} \ u \ s \ u \ t \ u = {}" by auto - show ?thesis unfolding uv1 uv2 * apply(rule **[OF d(5)[OF assms(2-4)]]) - defer apply(subst assms(5)[unfolded uv1 uv2]) unfolding uv1 uv2 by auto qed - -lemma division_split_right_inj: fixes type::"'a::ordered_euclidean_space" - assumes "d division_of i" "k1 \ d" "k2 \ d" "k1 \ k2" - "k1 \ {x::'a. x\k \ c} = k2 \ {x. x\k \ c}" and k:"k\Basis" - shows "content(k1 \ {x. x\k \ c}) = 0" -proof- note d=division_ofD[OF assms(1)] - have *:"\a b::'a. \ c. (content({a..b} \ {x. x\k >= c}) = 0 \ interior({a..b} \ {x. x\k >= c}) = {})" + have **: "\s t u. s \ t = {} \ u \ s \ u \ t \ u = {}" + by auto + show ?thesis + unfolding uv1 uv2 * apply(rule **[OF d(5)[OF assms(2-4)]]) + defer + apply (subst assms(5)[unfolded uv1 uv2]) + unfolding uv1 uv2 + apply auto + done +qed + +lemma division_split_right_inj: + fixes type :: "'a::ordered_euclidean_space" + assumes "d division_of i" + and "k1 \ d" + and "k2 \ d" + and "k1 \ k2" + and "k1 \ {x::'a. x\k \ c} = k2 \ {x. x\k \ c}" + and k: "k \ Basis" + shows "content (k1 \ {x. x\k \ c}) = 0" +proof - + note d=division_ofD[OF assms(1)] + have *: "\a b::'a. \c. content({a..b} \ {x. x\k \ c}) = 0 \ + interior({a..b} \ {x. x\k \ c}) = {}" unfolding interval_split[OF k] content_eq_0_interior by auto guess u1 v1 using d(4)[OF assms(2)] apply-by(erule exE)+ note uv1=this guess u2 v2 using d(4)[OF assms(3)] apply-by(erule exE)+ note uv2=this - have **:"\s t u. s \ t = {} \ u \ s \ u \ t \ u = {}" by auto - show ?thesis unfolding uv1 uv2 * apply(rule **[OF d(5)[OF assms(2-4)]]) - defer apply(subst assms(5)[unfolded uv1 uv2]) unfolding uv1 uv2 by auto qed - -lemma tagged_division_split_left_inj: fixes x1::"'a::ordered_euclidean_space" - assumes "d tagged_division_of i" "(x1,k1) \ d" "(x2,k2) \ d" "k1 \ k2" "k1 \ {x. x\k \ c} = k2 \ {x. x\k \ c}" - and k:"k\Basis" - shows "content(k1 \ {x. x\k \ c}) = 0" -proof- have *:"\a b c. (a,b) \ c \ b \ snd ` c" unfolding image_iff apply(rule_tac x="(a,b)" in bexI) by auto - show ?thesis apply(rule division_split_left_inj[OF division_of_tagged_division[OF assms(1)]]) - apply(rule_tac[1-2] *) using assms(2-) by auto qed - -lemma tagged_division_split_right_inj: fixes x1::"'a::ordered_euclidean_space" - assumes "d tagged_division_of i" "(x1,k1) \ d" "(x2,k2) \ d" "k1 \ k2" "k1 \ {x. x\k \ c} = k2 \ {x. x\k \ c}" - and k:"k\Basis" + have **: "\s t u. s \ t = {} \ u \ s \ u \ t \ u = {}" + by auto + show ?thesis + unfolding uv1 uv2 * + apply (rule **[OF d(5)[OF assms(2-4)]]) + defer + apply (subst assms(5)[unfolded uv1 uv2]) + unfolding uv1 uv2 + apply auto + done +qed + +lemma tagged_division_split_left_inj: + fixes x1 :: "'a::ordered_euclidean_space" + assumes "d tagged_division_of i" + and "(x1,k1) \ d" + and "(x2, k2) \ d" + and "k1 \ k2" + and "k1 \ {x. x\k \ c} = k2 \ {x. x\k \ c}" + and k: "k \ Basis" + shows "content (k1 \ {x. x\k \ c}) = 0" +proof - + have *: "\a b c. (a,b) \ c \ b \ snd ` c" + unfolding image_iff + apply (rule_tac x="(a,b)" in bexI) + apply auto + done + show ?thesis + apply (rule division_split_left_inj[OF division_of_tagged_division[OF assms(1)]]) + apply (rule_tac[1-2] *) + using assms(2-) + apply auto + done +qed + +lemma tagged_division_split_right_inj: + fixes x1 :: "'a::ordered_euclidean_space" + assumes "d tagged_division_of i" + and "(x1, k1) \ d" + and "(x2, k2) \ d" + and "k1 \ k2" + and "k1 \ {x. x\k \ c} = k2 \ {x. x\k \ c}" + and k: "k \ Basis" shows "content(k1 \ {x. x\k \ c}) = 0" -proof- have *:"\a b c. (a,b) \ c \ b \ snd ` c" unfolding image_iff apply(rule_tac x="(a,b)" in bexI) by auto - show ?thesis apply(rule division_split_right_inj[OF division_of_tagged_division[OF assms(1)]]) - apply(rule_tac[1-2] *) using assms(2-) by auto qed +proof - + have *: "\a b c. (a,b) \ c \ b \ snd ` c" + unfolding image_iff + apply (rule_tac x="(a,b)" in bexI) + apply auto + done + show ?thesis + apply (rule division_split_right_inj[OF division_of_tagged_division[OF assms(1)]]) + apply (rule_tac[1-2] *) + using assms(2-) + apply auto + done +qed lemma division_split: fixes a::"'a::ordered_euclidean_space" assumes "p division_of {a..b}" and k:"k\Basis" diff -r 6301ed01e34d -r 8adcf1f0042d src/Pure/System/cygwin_init.scala --- a/src/Pure/System/cygwin_init.scala Fri Sep 06 20:59:36 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,166 +0,0 @@ -/* Title: Pure/System/cygwin_init.scala - Author: Makarius - -Initialize Isabelle distribution after extracting via 7zip. -*/ - -package isabelle - - -import java.io.{File => JFile, BufferedReader, InputStreamReader} -import java.nio.file.{Paths, Files} -import java.awt.{GraphicsEnvironment, Point, Font} -import javax.swing.ImageIcon - -import scala.annotation.tailrec -import scala.swing.{ScrollPane, Button, FlowPanel, - BorderPanel, MainFrame, TextArea, SwingApplication} -import scala.swing.event.ButtonClicked - - -object Cygwin_Init -{ - /* main GUI entry point */ - - def main_frame(isabelle_home: String, start: => Unit) = new MainFrame - { - title = "Isabelle system initialization" - iconImage = new ImageIcon(isabelle_home + "\\lib\\logo\\isabelle.gif").getImage - - val layout_panel = new BorderPanel - contents = layout_panel - - - /* text area */ - - def echo(msg: String) { text_area.append(msg + "\n") } - - val text_area = new TextArea { - font = new Font("SansSerif", Font.PLAIN, GUI.resolution_scale(10) max 14) - editable = false - columns = 50 - rows = 15 - } - - layout_panel.layout(new ScrollPane(text_area)) = BorderPanel.Position.Center - - - /* exit button */ - - var _return_code: Option[Int] = None - def maybe_exit() - { - _return_code match { - case None => - case Some(0) => - visible = false - default_thread_pool.submit(() => start) - case Some(rc) => - sys.exit(rc) - } - } - - def return_code(rc: Int): Unit = - Swing_Thread.later { - _return_code = Some(rc) - button.peer.getRootPane.setDefaultButton(button.peer) - layout_panel.repaint - } - - override def closeOperation { maybe_exit() } - - val button = new Button { - text = "Done" - reactions += { case ButtonClicked(_) => maybe_exit() } - } - val button_panel = new FlowPanel(FlowPanel.Alignment.Center)(button) - - layout_panel.layout(button_panel) = BorderPanel.Position.South - - - /* show window */ - - pack() - val point = GraphicsEnvironment.getLocalGraphicsEnvironment().getCenterPoint() - location = new Point(point.x - size.width / 2, point.y - size.height / 2) - visible = true - - default_thread_pool.submit(() => - try { - init_filesystem(isabelle_home, echo) - return_code(0) - } - catch { - case exn: Throwable => - text_area.append("Error:\n" + Exn.message(exn) + "\n") - return_code(2) - } - ) - } - - - /* init Cygwin file-system */ - - private def init_filesystem(isabelle_home: String, echo: String => Unit) - { - val cygwin_root = isabelle_home + "\\contrib\\cygwin" - - def execute(args: String*): Int = - { - val cwd = new JFile(isabelle_home) - val env = Map("CYGWIN" -> "nodosfilewarning") - val proc = Isabelle_System.raw_execute(cwd, env, true, args: _*) - proc.getOutputStream.close - - val stdout = new BufferedReader(new InputStreamReader(proc.getInputStream, UTF8.charset)) - try { - var line = stdout.readLine - while (line != null) { - echo(line) - line = stdout.readLine - } - } - finally { stdout.close } - - proc.waitFor - } - - echo("Initializing Cygwin:") - - echo("symlinks ...") - val symlinks = - { - val path = (new JFile(cygwin_root + "\\isabelle\\symlinks")).toPath - Files.readAllLines(path, UTF8.charset).toArray.toList.asInstanceOf[List[String]] - } - @tailrec def recover_symlinks(list: List[String]): Unit = - { - list match { - case Nil | List("") => - case link :: content :: rest => - val path = (new JFile(isabelle_home, link)).toPath - - val writer = Files.newBufferedWriter(path, UTF8.charset) - try { writer.write("!" + content + "\0") } - finally { writer.close } - - Files.setAttribute(path, "dos:system", true) - - recover_symlinks(rest) - case _ => error("Unbalanced symlinks list") - } - } - recover_symlinks(symlinks) - - echo("rebaseall ...") - execute(cygwin_root + "\\bin\\dash.exe", "/isabelle/rebaseall") - - echo("postinstall ...") - execute(cygwin_root + "\\bin\\bash.exe", "/isabelle/postinstall") - - echo("init ...") - Isabelle_System.init() - echo("OK") - } -} - diff -r 6301ed01e34d -r 8adcf1f0042d src/Pure/System/gui.scala --- a/src/Pure/System/gui.scala Fri Sep 06 20:59:36 2013 +0200 +++ b/src/Pure/System/gui.scala Sat Sep 07 20:12:38 2013 +0200 @@ -114,7 +114,7 @@ /* icon */ def isabelle_icon(): ImageIcon = - new ImageIcon(Isabelle_System.platform_path(Path.explode("~~/lib/logo/isabelle.gif"))) + new ImageIcon(getClass.getClassLoader.getResource("isabelle/isabelle.gif")) def isabelle_image(): Image = isabelle_icon().getImage } diff -r 6301ed01e34d -r 8adcf1f0042d src/Pure/System/system_dialog.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/System/system_dialog.scala Sat Sep 07 20:12:38 2013 +0200 @@ -0,0 +1,212 @@ +/* Title: Pure/Tools/system_dialog.scala + Author: Makarius + +Dialog for system processes, with optional output window. +*/ + +package isabelle + + +import java.awt.{GraphicsEnvironment, Point, Font} +import javax.swing.WindowConstants +import java.io.{File => JFile, BufferedReader, InputStreamReader} + +import scala.swing.{ScrollPane, Button, CheckBox, FlowPanel, + BorderPanel, Frame, TextArea, Component, Label} +import scala.swing.event.ButtonClicked + + +class System_Dialog extends Build.Progress +{ + /* GUI state -- owned by Swing thread */ + + private var _title = "Isabelle" + private var _window: Option[Window] = None + private var _return_code: Option[Int] = None + + private def check_window(): Window = + { + Swing_Thread.require() + + _window match { + case Some(window) => window + case None => + val window = new Window + _window = Some(window) + + window.pack() + val point = GraphicsEnvironment.getLocalGraphicsEnvironment().getCenterPoint() + window.location = + new Point(point.x - window.size.width / 2, point.y - window.size.height / 2) + window.visible = true + + window + } + } + + private val result = Future.promise[Int] + + private def conclude() + { + Swing_Thread.require() + require(_return_code.isDefined) + + _window match { + case None => + case Some(window) => + window.visible = false + window.dispose + _window = None + } + + try { result.fulfill(_return_code.get) } + catch { case ERROR(_) => } + } + + def join(): Int = result.join + def join_exit(): Nothing = sys.exit(join) + + + /* window */ + + private class Window extends Frame + { + title = _title + iconImage = GUI.isabelle_image() + + + /* text */ + + val text = new TextArea { + font = new Font("SansSerif", Font.PLAIN, GUI.resolution_scale(10) max 14) + editable = false + columns = 50 + rows = 20 + } + + val scroll_text = new ScrollPane(text) + + + /* layout panel with dynamic actions */ + + val action_panel = new FlowPanel(FlowPanel.Alignment.Center)() + val layout_panel = new BorderPanel + layout_panel.layout(scroll_text) = BorderPanel.Position.Center + layout_panel.layout(action_panel) = BorderPanel.Position.South + + contents = layout_panel + + def set_actions(cs: Component*) + { + action_panel.contents.clear + action_panel.contents ++= cs + layout_panel.revalidate + layout_panel.repaint + } + + + /* close */ + + peer.setDefaultCloseOperation(WindowConstants.DO_NOTHING_ON_CLOSE) + + override def closeOperation { + if (_return_code.isDefined) conclude() + else stopping() + } + + def stopping() + { + is_stopped = true + set_actions(new Label("Stopping ...")) + } + + val stop_button = new Button("Stop") { + reactions += { case ButtonClicked(_) => stopping() } + } + + var do_auto_close = true + def can_auto_close: Boolean = do_auto_close && _return_code == Some(0) + + val auto_close = new CheckBox("Auto close") { + reactions += { + case ButtonClicked(_) => do_auto_close = this.selected + if (can_auto_close) conclude() + } + } + auto_close.selected = do_auto_close + auto_close.tooltip = "Automatically close dialog when finished" + + set_actions(stop_button, auto_close) + + + /* exit */ + + val delay_exit = + Swing_Thread.delay_first(Time.seconds(1.0)) + { + if (can_auto_close) conclude() + else { + val button = + new Button(if (_return_code == Some(0)) "OK" else "Exit") { + reactions += { case ButtonClicked(_) => conclude() } + } + set_actions(button) + button.peer.getRootPane.setDefaultButton(button.peer) + } + } + } + + + /* progress operations */ + + def title(txt: String): Unit = + Swing_Thread.later { + _title = txt + _window.foreach(window => window.title = txt) + } + + def return_code(rc: Int): Unit = + Swing_Thread.later { + _return_code = Some(rc) + _window match { + case None => conclude() + case Some(window) => window.delay_exit.invoke + } + } + + override def echo(txt: String): Unit = + Swing_Thread.later { + val window = check_window() + window.text.append(txt + "\n") + val vertical = window.scroll_text.peer.getVerticalScrollBar + vertical.setValue(vertical.getMaximum) + } + + override def theory(session: String, theory: String): Unit = + echo(session + ": theory " + theory) + + @volatile private var is_stopped = false + override def stopped: Boolean = is_stopped + + + /* system operations */ + + def execute(cwd: JFile, env: Map[String, String], args: String*): Int = + { + val proc = Isabelle_System.raw_execute(cwd, env, true, args: _*) + proc.getOutputStream.close + + val stdout = new BufferedReader(new InputStreamReader(proc.getInputStream, UTF8.charset)) + try { + var line = stdout.readLine + while (line != null) { + echo(line) + line = stdout.readLine + } + } + finally { stdout.close } + + proc.waitFor + } +} + diff -r 6301ed01e34d -r 8adcf1f0042d src/Pure/Tools/build_dialog.scala --- a/src/Pure/Tools/build_dialog.scala Fri Sep 06 20:59:36 2013 +0200 +++ b/src/Pure/Tools/build_dialog.scala Sat Sep 07 20:12:38 2013 +0200 @@ -16,7 +16,9 @@ object Build_Dialog { - def main(args: Array[String]) = + /* command line entry point */ + + def main(args: Array[String]) { GUI.init_laf() try { @@ -26,26 +28,16 @@ logic :: Properties.Value.Boolean(system_mode) :: include_dirs => - val more_dirs = include_dirs.map(s => ((false, Path.explode(s)))) - val options = Options.init() + val dirs = include_dirs.map(Path.explode(_)) val session = Isabelle_System.default_logic(logic, if (logic_option != "") options.string(logic_option) else "") - if (Build.build(options = options, build_heap = true, no_build = true, - more_dirs = more_dirs, sessions = List(session)) == 0) sys.exit(0) - else - Swing_Thread.later { - val top = build_dialog(options, system_mode, more_dirs, session) - top.pack() + val system_dialog = new System_Dialog + dialog(options, system_dialog, system_mode, dirs, session) + system_dialog.join_exit - val point = GraphicsEnvironment.getLocalGraphicsEnvironment().getCenterPoint() - top.location = - new Point(point.x - top.size.width / 2, point.y - top.size.height / 2) - - top.visible = true - } case _ => error("Bad arguments:\n" + cat_lines(args)) } } @@ -57,127 +49,36 @@ } - def build_dialog( - options: Options, - system_mode: Boolean, - more_dirs: List[(Boolean, Path)], - session: String): MainFrame = new MainFrame - { - iconImage = GUI.isabelle_image() - - - /* GUI state */ - - @volatile private var is_stopped = false - private var return_code = 2 - - override def closeOperation { sys.exit(return_code) } - - - /* text */ - - val text = new TextArea { - font = new Font("SansSerif", Font.PLAIN, GUI.resolution_scale(10) max 14) - editable = false - columns = 50 - rows = 20 - } - - val scroll_text = new ScrollPane(text) - - val progress = new Build.Progress - { - override def echo(msg: String): Unit = - Swing_Thread.later { - text.append(msg + "\n") - val vertical = scroll_text.peer.getVerticalScrollBar - vertical.setValue(vertical.getMaximum) - } - override def theory(session: String, theory: String): Unit = - echo(session + ": theory " + theory) - override def stopped: Boolean = is_stopped - } - - - /* layout panel with dynamic actions */ - - val action_panel = new FlowPanel(FlowPanel.Alignment.Center)() - val layout_panel = new BorderPanel - layout_panel.layout(scroll_text) = BorderPanel.Position.Center - layout_panel.layout(action_panel) = BorderPanel.Position.South - - contents = layout_panel + /* dialog */ - def set_actions(cs: Component*) - { - action_panel.contents.clear - action_panel.contents ++= cs - layout_panel.revalidate - layout_panel.repaint - } - - - /* actions */ - - var do_auto_close = true - def check_auto_close(): Unit = if (do_auto_close && return_code == 0) sys.exit(return_code) - - val auto_close = new CheckBox("Auto close") { - reactions += { - case ButtonClicked(_) => do_auto_close = this.selected - check_auto_close() - } - } - auto_close.selected = do_auto_close - auto_close.tooltip = "Automatically close dialog when finished" - + def dialog( + options: Options, + system_dialog: System_Dialog, + system_mode: Boolean, + dirs: List[Path], + session: String) + { + val more_dirs = dirs.map((false, _)) - val stop_button = new Button("Stop") { - reactions += { - case ButtonClicked(_) => - is_stopped = true - set_actions(new Label("Stopping ...")) - } - } - - set_actions(stop_button, auto_close) - - - /* exit */ + if (Build.build(options = options, build_heap = true, no_build = true, + more_dirs = more_dirs, sessions = List(session)) == 0) + system_dialog.return_code(0) + else { + system_dialog.title("Isabelle build (" + Isabelle_System.getenv("ML_IDENTIFIER") + ")") + system_dialog.echo("Build started for Isabelle/" + session + " ...") - val delay_exit = - Swing_Thread.delay_first(Time.seconds(1.0)) - { - check_auto_close() - val button = - new Button(if (return_code == 0) "OK" else "Exit") { - reactions += { case ButtonClicked(_) => sys.exit(return_code) } - } - set_actions(button) - button.peer.getRootPane.setDefaultButton(button.peer) - } - - - /* main build */ - - title = "Isabelle build (" + Isabelle_System.getenv("ML_IDENTIFIER") + ")" - progress.echo("Build started for Isabelle/" + session + " ...") - - default_thread_pool.submit(() => { val (out, rc) = try { ("", - Build.build(options = options, progress = progress, + Build.build(options = options, progress = system_dialog, build_heap = true, more_dirs = more_dirs, system_mode = system_mode, sessions = List(session))) } catch { case exn: Throwable => (Exn.message(exn) + "\n", 2) } - Swing_Thread.now { - progress.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n")) - return_code = rc - delay_exit.invoke() - } - }) + + system_dialog.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n")) + system_dialog.return_code(rc) + } } } diff -r 6301ed01e34d -r 8adcf1f0042d src/Pure/Tools/keywords.scala --- a/src/Pure/Tools/keywords.scala Fri Sep 06 20:59:36 2013 +0200 +++ b/src/Pure/Tools/keywords.scala Sat Sep 07 20:12:38 2013 +0200 @@ -4,6 +4,8 @@ Generate keyword files for Emacs Proof General. */ +/*Proof General legacy*/ + package isabelle diff -r 6301ed01e34d -r 8adcf1f0042d src/Pure/Tools/main.scala --- a/src/Pure/Tools/main.scala Fri Sep 06 20:59:36 2013 +0200 +++ b/src/Pure/Tools/main.scala Sat Sep 07 20:12:38 2013 +0200 @@ -7,68 +7,192 @@ package isabelle -import java.lang.System -import java.io.{File => JFile} +import javax.swing.SwingUtilities +import java.lang.{System, ClassLoader} +import java.io.{File => JFile, BufferedReader, InputStreamReader} +import java.nio.file.Files + +import scala.annotation.tailrec object Main { + /** main entry point **/ + def main(args: Array[String]) { - def start: Unit = + val system_dialog = new System_Dialog + + def exit_error(exn: Throwable): Nothing = + { + GUI.dialog(null, "Isabelle", GUI.scrollable_text(Exn.message(exn))) + system_dialog.return_code(2) + system_dialog.join_exit + } + + def build { - val (out, rc) = - try { - GUI.init_laf() - Isabelle_System.init() - Isabelle_System.isabelle_tool("jedit", ("-s" :: "--" :: args.toList): _*) + try { + GUI.init_laf() + Isabelle_System.init() + + val mode = Isabelle_System.getenv("JEDIT_BUILD_MODE") + if (mode == "none") + system_dialog.return_code(0) + else { + val system_mode = mode == "" || mode == "system" + val dirs = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS")) + val options = Options.init() + val session = Isabelle_System.default_logic( + Isabelle_System.getenv("JEDIT_LOGIC"), + options.string("jedit_logic")) + Build_Dialog.dialog(options, system_dialog, system_mode, dirs, session) } - catch { case exn: Throwable => (Exn.message(exn), 2) } + } + catch { case exn: Throwable => exit_error(exn) } + } + + def start + { + val do_start = + { + try { + /* settings directory */ + + val settings_dir = Path.explode("$JEDIT_SETTINGS") + Isabelle_System.mkdirs(settings_dir + Path.explode("DockableWindowManager")) + + if (!(settings_dir + Path.explode("perspective.xml")).is_file) { + File.write(settings_dir + Path.explode("DockableWindowManager/perspective-view0.xml"), + """""") + File.write(settings_dir + Path.explode("perspective.xml"), + """ + + + + + +""") + } + - if (rc != 0) - GUI.dialog(null, "Isabelle", "Isabelle output", - GUI.scrollable_text(out + "\nReturn code: " + rc)) + /* args */ + + val jedit_options = + Isabelle_System.getenv_strict("JEDIT_OPTIONS").split(" +") + + val jedit_settings = + Array("-settings=" + Isabelle_System.platform_path(Path.explode("$JEDIT_SETTINGS"))) + + val more_args = + if (args.isEmpty) + Array(Isabelle_System.platform_path(Path.explode("$USER_HOME/Scratch.thy"))) + else args + - sys.exit(rc) + /* startup */ + + System.setProperty("jedit.home", + Isabelle_System.platform_path(Path.explode("$JEDIT_HOME/dist"))) + + System.setProperty("scala.home", + Isabelle_System.platform_path(Path.explode("$SCALA_HOME"))) + + val jedit = ClassLoader.getSystemClassLoader.loadClass("org.gjt.sp.jedit.jEdit") + val jedit_main = jedit.getDeclaredMethod("main", classOf[Array[String]]) + + () => jedit_main.invoke(null, jedit_options ++ jedit_settings ++ more_args) + } + catch { case exn: Throwable => exit_error(exn) } + } + do_start() } if (Platform.is_windows) { - val init_isabelle_home = - try { - GUI.init_laf() + try { + GUI.init_laf() - val isabelle_home0 = System.getenv("ISABELLE_HOME_WINDOWS") - val isabelle_home = System.getProperty("isabelle.home") + val isabelle_home0 = System.getenv("ISABELLE_HOME_WINDOWS") + val isabelle_home = System.getProperty("isabelle.home") - if (isabelle_home0 != null && isabelle_home0 != "") None - else { - if (isabelle_home == null || isabelle_home == "") - error("Unknown Isabelle home directory") - if (!(new JFile(isabelle_home)).isDirectory) - error("Bad Isabelle home directory: " + quote(isabelle_home)) + if (isabelle_home0 == null || isabelle_home0 == "") { + if (isabelle_home == null || isabelle_home == "") + error("Unknown Isabelle home directory") + if (!(new JFile(isabelle_home)).isDirectory) + error("Bad Isabelle home directory: " + quote(isabelle_home)) - val cygwin_root = isabelle_home + "\\contrib\\cygwin" - if ((new JFile(cygwin_root)).isDirectory) - System.setProperty("cygwin.root", cygwin_root) + val cygwin_root = isabelle_home + "\\contrib\\cygwin" + if ((new JFile(cygwin_root)).isDirectory) + System.setProperty("cygwin.root", cygwin_root) - val uninitialized_file = new JFile(cygwin_root, "isabelle\\uninitialized") - val uninitialized = uninitialized_file.isFile && uninitialized_file.delete + val uninitialized_file = new JFile(cygwin_root, "isabelle\\uninitialized") + val uninitialized = uninitialized_file.isFile && uninitialized_file.delete - if (uninitialized) Some(isabelle_home) else None - } + if (uninitialized) cygwin_init(system_dialog, isabelle_home, cygwin_root) } - catch { - case exn: Throwable => - GUI.dialog(null, "Isabelle", GUI.scrollable_text(Exn.message(exn))) - sys.exit(2) - } - init_isabelle_home match { - case Some(isabelle_home) => - Swing_Thread.later { Cygwin_Init.main_frame(isabelle_home, start) } - case None => start + } + catch { case exn: Throwable => exit_error(exn) } + + if (system_dialog.stopped) { + system_dialog.return_code(130) + system_dialog.join_exit } } - else start + + build + val rc = system_dialog.join + if (rc == 0) start else sys.exit(rc) + } + + + + /** Cygwin init (e.g. after extraction via 7zip) **/ + + private def cygwin_init(system_dialog: System_Dialog, isabelle_home: String, cygwin_root: String) + { + system_dialog.title("Isabelle system initialization") + system_dialog.echo("Initializing Cygwin ...") + + def execute(args: String*): Int = + { + val cwd = new JFile(isabelle_home) + val env = Map("CYGWIN" -> "nodosfilewarning") + system_dialog.execute(cwd, env, args: _*) + } + + system_dialog.echo("symlinks ...") + val symlinks = + { + val path = (new JFile(cygwin_root + "\\isabelle\\symlinks")).toPath + Files.readAllLines(path, UTF8.charset).toArray.toList.asInstanceOf[List[String]] + } + @tailrec def recover_symlinks(list: List[String]): Unit = + { + list match { + case Nil | List("") => + case link :: content :: rest => + val path = (new JFile(isabelle_home, link)).toPath + + val writer = Files.newBufferedWriter(path, UTF8.charset) + try { writer.write("!" + content + "\0") } + finally { writer.close } + + Files.setAttribute(path, "dos:system", true) + + recover_symlinks(rest) + case _ => error("Unbalanced symlinks list") + } + } + recover_symlinks(symlinks) + + system_dialog.echo("rebaseall ...") + execute(cygwin_root + "\\bin\\dash.exe", "/isabelle/rebaseall") + + system_dialog.echo("postinstall ...") + execute(cygwin_root + "\\bin\\bash.exe", "/isabelle/postinstall") + + system_dialog.echo("init ...") + Isabelle_System.init() } } diff -r 6301ed01e34d -r 8adcf1f0042d src/Pure/build-jars --- a/src/Pure/build-jars Fri Sep 06 20:59:36 2013 +0200 +++ b/src/Pure/build-jars Sat Sep 07 20:12:38 2013 +0200 @@ -47,7 +47,6 @@ PIDE/yxml.scala System/color_value.scala System/command_line.scala - System/cygwin_init.scala System/event_bus.scala System/gui.scala System/gui_setup.scala @@ -64,6 +63,7 @@ System/session.scala System/swing_thread.scala System/system_channel.scala + System/system_dialog.scala System/utf8.scala Thy/html.scala Thy/present.scala @@ -232,6 +232,8 @@ mkdir -p "$(dirname "$CHARSET_SERVICE")" echo isabelle.Isabelle_Charset_Provider > "$CHARSET_SERVICE" + cp "$ISABELLE_HOME/lib/logo/isabelle.gif" isabelle/. + isabelle_jdk jar cfe "$(jvmpath "$TARGET")" isabelle.GUI_Setup META-INF isabelle || \ fail "Failed to produce $TARGET" diff -r 6301ed01e34d -r 8adcf1f0042d src/Tools/Graphview/lib/Tools/graphview --- a/src/Tools/Graphview/lib/Tools/graphview Fri Sep 06 20:59:36 2013 +0200 +++ b/src/Tools/Graphview/lib/Tools/graphview Sat Sep 07 20:12:38 2013 +0200 @@ -139,6 +139,10 @@ rm -rf classes && mkdir classes ( + #workaround for scalac + function stty() { :; } + export -f stty + CLASSPATH="$CLASSPATH:$PURE_JAR" CLASSPATH="$(jvmpath "$CLASSPATH")" exec "$SCALA_HOME/bin/scalac" $ISABELLE_SCALA_BUILD_OPTIONS -d classes "${SOURCES[@]}" diff -r 6301ed01e34d -r 8adcf1f0042d src/Tools/jEdit/lib/Tools/jedit --- a/src/Tools/jEdit/lib/Tools/jedit Fri Sep 06 20:59:36 2013 +0200 +++ b/src/Tools/jEdit/lib/Tools/jedit Sat Sep 07 20:12:38 2013 +0200 @@ -26,7 +26,6 @@ "src/isabelle_sidekick.scala" "src/jedit_editor.scala" "src/jedit_lib.scala" - "src/jedit_main.scala" "src/jedit_options.scala" "src/jedit_thy_load.scala" "src/monitor_dockable.scala" @@ -109,14 +108,12 @@ # options -declare -a BUILD_DIALOG_OPTIONS=(-L jedit_logic) - BUILD_ONLY=false BUILD_JARS="jars" JEDIT_SESSION_DIRS="" JEDIT_LOGIC="" JEDIT_PRINT_MODE="" -NO_BUILD="false" +JEDIT_BUILD_MODE="normal" function getoptions() { @@ -136,8 +133,6 @@ else JEDIT_SESSION_DIRS="$JEDIT_SESSION_DIRS:$OPTARG" fi - BUILD_DIALOG_OPTIONS["${#BUILD_DIALOG_OPTIONS[@]}"]="-d" - BUILD_DIALOG_OPTIONS["${#BUILD_DIALOG_OPTIONS[@]}"]="$OPTARG" ;; f) BUILD_JARS="jars_fresh" @@ -146,8 +141,6 @@ ARGS["${#ARGS[@]}"]="$OPTARG" ;; l) - BUILD_DIALOG_OPTIONS["${#BUILD_DIALOG_OPTIONS[@]}"]="-l" - BUILD_DIALOG_OPTIONS["${#BUILD_DIALOG_OPTIONS[@]}"]="$OPTARG" JEDIT_LOGIC="$OPTARG" ;; m) @@ -158,10 +151,10 @@ fi ;; n) - NO_BUILD="true" + JEDIT_BUILD_MODE="none" ;; s) - BUILD_DIALOG_OPTIONS["${#BUILD_DIALOG_OPTIONS[@]}"]="-s" + JEDIT_BUILD_MODE="system" ;; \?) usage @@ -171,9 +164,8 @@ } declare -a JAVA_ARGS; eval "JAVA_ARGS=($JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS)" -[ -n "$SCALA_HOME" ] && JAVA_ARGS["${#JAVA_ARGS[@]}"]="-Dscala.home=$SCALA_HOME" -declare -a ARGS; eval "ARGS=($JEDIT_OPTIONS)" +declare -a ARGS=() declare -a OPTIONS; eval "OPTIONS=($ISABELLE_JEDIT_OPTIONS)" getoptions "${OPTIONS[@]}" @@ -301,8 +293,12 @@ cp -p -R -f "${JEDIT_JARS[@]}" dist/jars/. || failed ( - for JAR in "$JEDIT_JAR" "${JEDIT_JARS[@]}" "${JFREECHART_JARS[@]}" "$XZ_JAVA_HOME/lib/xz.jar" \ - "$PURE_JAR" "$GRAPHVIEW_JAR" "$SCALA_HOME/lib/scala-compiler.jar" + #workaround for scalac + function stty() { :; } + export -f stty + + for JAR in "$JEDIT_JAR" "${JEDIT_JARS[@]}" "${JFREECHART_JARS[@]}" \ + "$XZ_JAVA_HOME/lib/xz.jar" "$PURE_JAR" "$GRAPHVIEW_JAR" "$SCALA_HOME/lib/scala-compiler.jar" do CLASSPATH="$CLASSPATH:$JAR" done @@ -322,32 +318,8 @@ ## main if [ "$BUILD_ONLY" = false ]; then - mkdir -p "$JEDIT_SETTINGS/DockableWindowManager" - - if [ ! -e "$JEDIT_SETTINGS/perspective.xml" ]; then - cat > "$JEDIT_SETTINGS/DockableWindowManager/perspective-view0.xml" < -EOF - cat > "$JEDIT_SETTINGS/perspective.xml" < - - - - - - -EOF - fi - - if [ "$NO_BUILD" = false ]; then - "$ISABELLE_TOOL" build_dialog "${BUILD_DIALOG_OPTIONS[@]}" - RC="$?" - [ "$RC" = 0 ] || exit "$RC" - fi - - export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_PRINT_MODE + export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_PRINT_MODE JEDIT_BUILD_MODE exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" \ - -jar "$(jvmpath "$JEDIT_HOME/dist/jedit.jar")" \ - "-settings=$(jvmpath "$JEDIT_SETTINGS")" "${ARGS[@]}" + -classpath "$(jvmpath "$JEDIT_HOME/dist/jedit.jar")" isabelle.Main "${ARGS[@]}" fi diff -r 6301ed01e34d -r 8adcf1f0042d src/Tools/jEdit/src/jedit_main.scala --- a/src/Tools/jEdit/src/jedit_main.scala Fri Sep 06 20:59:36 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,33 +0,0 @@ -/* Title: Tools/jEdit/src/jedit_main.scala - Author: Makarius - -Main entry point from running JVM. -*/ - -package isabelle.jedit - - -import isabelle._ - - -import org.gjt.sp.jedit.jEdit - - -object JEdit_Main -{ - def main(args: Array[String]) - { - GUI.init_laf() - Isabelle_System.init() - - System.setProperty("jedit.home", - Isabelle_System.platform_path(Path.explode("$JEDIT_HOME/dist"))) - - // FIXME properties from JEDIT_JAVA_OPTIONS JEDIT_SYSTEM_OPTIONS - val jedit_options = Isabelle_System.getenv_strict("JEDIT_OPTIONS").split(" +") - val jedit_settings = - Array("-settings=" + Isabelle_System.platform_path(Path.explode("$JEDIT_SETTINGS"))) - jEdit.main(jedit_options ++ jedit_settings ++ args) - } -} -