--- 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 @@
<string>isabelle.Main</string>
<key>JVMOptions</key>
<array>
-<string>-Dapple.laf.useScreenMenuBar=true</string>
+<string>-Dapple.laf.useScreenMenuBar=true -Xms128m -Xmx1024m -Xss2m -Dactors.corePoolSize=4 -Dactors.enableForkJoin=false</string>
<string>-Disabelle.home=$APP_ROOT/Contents/Resources/{ISABELLE_NAME}</string>
</array>
<key>JVMArguments</key>
--- 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 @@
<classPath>
<mainClass>isabelle.Main</mainClass>
<cp>%EXEDIR%\lib\classes\ext\Pure.jar</cp>
+ <cp>%EXEDIR%\lib\classes\ext\scala-compiler.jar</cp>
<cp>%EXEDIR%\lib\classes\ext\scala-library.jar</cp>
<cp>%EXEDIR%\lib\classes\ext\scala-swing.jar</cp>
+ <cp>%EXEDIR%\lib\classes\ext\scala-actors.jar</cp>
+ <cp>%EXEDIR%\lib\classes\ext\scala-reflect.jar</cp>
+ <cp>%EXEDIR%\src\Tools\jEdit\dist\jedit.jar</cp>
</classPath>
<jre>
<path>%EXEDIR%\contrib\jdk\x86-cygwin</path>
<minVersion></minVersion>
<maxVersion></maxVersion>
<jdkPreference>jdkOnly</jdkPreference>
- <opt>-Disabelle.home="%EXEDIR%"</opt>
+ <opt>-Dfile.encoding=UTF-8 -server -Xms128m -Xmx1024m -Xss2m -Dactors.corePoolSize=4 -Dactors.enableForkJoin=false -Disabelle.home="%EXEDIR%"</opt>
</jre>
<splash>
<file>isabelle.bmp</file>
--- 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
--- 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
--- 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
--- 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" <<EOF
+#!/usr/bin/env bash
+
+ISABELLE_TOOL="\$(dirname "\$0")"/bin/isabelle
+JEDIT_HOME="\$("\$ISABELLE_TOOL" getenv -b JEDIT_HOME)"
+
+exec "\$ISABELLE_TOOL" java -classpath "\$JEDIT_HOME/dist/jedit.jar" isabelle.Main "\$@"
+EOF
+ chmod +x "$ISABELLE_TARGET/$ISABELLE_NAME"
;;
macos)
purge_contrib '-name "x86*-linux" -o -name "x86*-cygwin" -o -name "x86*-windows"'
@@ -134,14 +143,14 @@
perl -pi -e "s,lookAndFeel=.*,lookAndFeel=com.apple.laf.AquaLookAndFeel,g;" \
-e "s,delete-line.shortcut=.*,delete-line.shortcut=C+d,g;" \
-e "s,delete.shortcut2=.*,delete.shortcut2=A+d,g;" \
- "$TMP/$ISABELLE_NAME/src/Tools/jEdit/dist/properties/jEdit.props"
+ "$ISABELLE_TARGET/src/Tools/jEdit/dist/properties/jEdit.props"
;;
windows)
purge_contrib '-name "x86*-linux" -o -name "x86*-darwin"'
mv "$ISABELLE_TARGET/contrib/windows_app" "$TMP/."
perl -pi -e "s,lookAndFeel=.*,lookAndFeel=com.sun.java.swing.plaf.windows.WindowsLookAndFeel,g;" \
- "$TMP/$ISABELLE_NAME/src/Tools/jEdit/dist/properties/jEdit.props"
+ "$ISABELLE_TARGET/src/Tools/jEdit/dist/properties/jEdit.props"
cp "$TMP/windows_app/Isabelle.exe" "$ISABELLE_TARGET/${ISABELLE_NAME}.exe"
cp "$ISABELLE_HOME/Admin/Windows/Cygwin/Cygwin-Setup.bat" \
@@ -204,10 +213,11 @@
cat "$APP_TEMPLATE/Info.plist" | \
perl -p -e "s,{ISABELLE_NAME},${ISABELLE_NAME},g;" > "$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/."
--- 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 -- "$@"
-
--- 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 \<Rightarrow> 'a::{real_normed_vector,complete_space}"
+lemma integrable_cauchy:
+ fixes f :: "'n::ordered_euclidean_space \<Rightarrow> 'a::{real_normed_vector,complete_space}"
shows "f integrable_on {a..b} \<longleftrightarrow>
- (\<forall>e>0.\<exists>d. gauge d \<and> (\<forall>p1 p2. p1 tagged_division_of {a..b} \<and> d fine p1 \<and>
- p2 tagged_division_of {a..b} \<and> d fine p2
- \<longrightarrow> norm(setsum (\<lambda>(x,k). content k *\<^sub>R f x) p1 -
- setsum (\<lambda>(x,k). content k *\<^sub>R f x) p2) < e))" (is "?l = (\<forall>e>0. \<exists>d. ?P e d)")
-proof assume ?l
+ (\<forall>e>0.\<exists>d. gauge d \<and>
+ (\<forall>p1 p2. p1 tagged_division_of {a..b} \<and> d fine p1 \<and>
+ p2 tagged_division_of {a..b} \<and> d fine p2 \<longrightarrow>
+ norm (setsum (\<lambda>(x,k). content k *\<^sub>R f x) p1 -
+ setsum (\<lambda>(x,k). content k *\<^sub>R f x) p2) < e))"
+ (is "?l = (\<forall>e>0. \<exists>d. ?P e d)")
+proof
+ assume ?l
then guess y unfolding integrable_on_def has_integral .. note y=this
- show "\<forall>e>0. \<exists>d. ?P e d" proof(rule,rule) case goal1 hence "e/2 > 0" by auto
+ show "\<forall>e>0. \<exists>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 ((\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>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 "\<forall>e>0. \<exists>d. ?P e d" hence "\<forall>n::nat. \<exists>d. ?P (inverse(real (n + 1))) d" by auto
+ qed
+ qed
+next
+ assume "\<forall>e>0. \<exists>d. ?P e d"
+ then have "\<forall>n::nat. \<exists>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 "\<And>n. gauge (\<lambda>x. \<Inter>{d i x |i. i \<in> {0..n}})" apply(rule gauge_inters) using d(1) by auto
- hence "\<forall>n. \<exists>p. p tagged_division_of {a..b} \<and> (\<lambda>x. \<Inter>{d i x |i. i \<in> {0..n}}) fine p" apply-
- proof case goal1 from this[of n] show ?case apply(drule_tac fine_division_exists) by auto qed
+ have "\<And>n. gauge (\<lambda>x. \<Inter>{d i x |i. i \<in> {0..n}})"
+ apply (rule gauge_inters)
+ using d(1)
+ apply auto
+ done
+ then have "\<forall>n. \<exists>p. p tagged_division_of {a..b} \<and> (\<lambda>x. \<Inter>{d i x |i. i \<in> {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:"\<And>i n. i\<le>n \<Longrightarrow> d i fine p n" using p(2) unfolding fine_inters by auto
+ have dp: "\<And>i n. i\<le>n \<Longrightarrow> d i fine p n"
+ using p(2) unfolding fine_inters by auto
have "Cauchy (\<lambda>n. setsum (\<lambda>(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 \<le> m" "N \<le> 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 \<le> m" "N \<le> n"
+ have *: "N = (N - 1) + 1" using N by auto
show "norm ((\<Sum>(x, k)\<in>p m. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>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 "\<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of {a..b} \<and> d fine p \<longrightarrow> norm ((\<Sum>(x, k)\<in>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 ((\<Sum>(x, k)\<in>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 "\<exists>d. gauge d \<and>
+ (\<forall>p. p tagged_division_of {a..b} \<and> d fine p \<longrightarrow> norm ((\<Sum>(x, k)\<in>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 ((\<Sum>(x, k)\<in>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 \<in> Basis"
+ fixes a :: "'a::ordered_euclidean_space"
+ assumes "k \<in> Basis"
shows
"{a..b} \<inter> {x. x\<bullet>k \<le> c} = {a .. (\<Sum>i\<in>Basis. (if i = k then min (b\<bullet>k) c else b\<bullet>i) *\<^sub>R i)}"
"{a..b} \<inter> {x. x\<bullet>k \<ge> c} = {(\<Sum>i\<in>Basis. (if i = k then max (a\<bullet>k) c else a\<bullet>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\<in>Basis" shows
- "content {a..b} = content({a..b} \<inter> {x. x\<bullet>k \<le> c}) + content({a..b} \<inter> {x. x\<bullet>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 \<in> Basis"
+ shows "content {a..b} = content({a..b} \<inter> {x. x\<bullet>k \<le> c}) + content({a..b} \<inter> {x. x\<bullet>k \<ge> c})"
proof cases
note simps = interval_split[OF assms] content_closed_interval_cases eucl_le[where 'a='a]
- have *:"Basis = insert k (Basis - {k})" "\<And>x. finite (Basis-{x})" "\<And>x. x\<notin>Basis-{x}"
+ have *: "Basis = insert k (Basis - {k})" "\<And>x. finite (Basis-{x})" "\<And>x. x\<notin>Basis-{x}"
using assms by auto
- have *:"\<And>X Y Z. (\<Prod>i\<in>Basis. Z i (if i = k then X else Y i)) = Z k X * (\<Prod>i\<in>Basis-{k}. Z i (Y i))"
+ have *: "\<And>X Y Z. (\<Prod>i\<in>Basis. Z i (if i = k then X else Y i)) = Z k X * (\<Prod>i\<in>Basis-{k}. Z i (Y i))"
"(\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i) = (\<Prod>i\<in>Basis-{k}. b\<bullet>i - a\<bullet>i) * (b\<bullet>k - a\<bullet>k)"
- apply(subst *(1)) defer apply(subst *(1)) unfolding setprod_insert[OF *(2-)] by auto
- assume as:"a\<le>b" moreover have "\<And>x. min (b \<bullet> k) c = max (a \<bullet> k) c
- \<Longrightarrow> x* (b\<bullet>k - a\<bullet>k) = x*(max (a \<bullet> k) c - a \<bullet> k) + x*(b \<bullet> k - max (a \<bullet> k) c)"
- by (auto simp add:field_simps)
- moreover have **:"(\<Prod>i\<in>Basis. ((\<Sum>i\<in>Basis. (if i = k then min (b \<bullet> k) c else b \<bullet> i) *\<^sub>R i) \<bullet> i - a \<bullet> i)) =
+ apply (subst *(1))
+ defer
+ apply (subst *(1))
+ unfolding setprod_insert[OF *(2-)]
+ apply auto
+ done
+ assume as: "a \<le> b"
+ moreover
+ have "\<And>x. min (b \<bullet> k) c = max (a \<bullet> k) c \<Longrightarrow>
+ x * (b\<bullet>k - a\<bullet>k) = x * (max (a \<bullet> k) c - a \<bullet> k) + x * (b \<bullet> k - max (a \<bullet> k) c)"
+ by (auto simp add: field_simps)
+ moreover
+ have **: "(\<Prod>i\<in>Basis. ((\<Sum>i\<in>Basis. (if i = k then min (b \<bullet> k) c else b \<bullet> i) *\<^sub>R i) \<bullet> i - a \<bullet> i)) =
(\<Prod>i\<in>Basis. (if i = k then min (b \<bullet> k) c else b \<bullet> i) - a \<bullet> i)"
"(\<Prod>i\<in>Basis. b \<bullet> i - ((\<Sum>i\<in>Basis. (if i = k then max (a \<bullet> k) c else a \<bullet> i) *\<^sub>R i) \<bullet> i)) =
(\<Prod>i\<in>Basis. b \<bullet> i - (if i = k then max (a \<bullet> k) c else a \<bullet> i))"
by (auto intro!: setprod_cong)
have "\<not> a \<bullet> k \<le> c \<Longrightarrow> \<not> c \<le> b \<bullet> k \<Longrightarrow> 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 "\<lambda>i x. b\<bullet>i - x"] *(1)[of "\<lambda>i x. x - a\<bullet>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 "\<lambda>i x. b\<bullet>i - x"] *(1)[of "\<lambda>i x. x - a\<bullet>i"]
+ unfolding *(2)
by auto
next
- assume "\<not> a \<le> b" then have "{a .. b} = {}"
+ assume "\<not> a \<le> 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 \<in> d" "k2 \<in> d" "k1 \<noteq> k2"
- "k1 \<inter> {x::'a. x\<bullet>k \<le> c} = k2 \<inter> {x. x\<bullet>k \<le> c}"and k:"k\<in>Basis"
+lemma division_split_left_inj:
+ fixes type :: "'a::ordered_euclidean_space"
+ assumes "d division_of i"
+ and "k1 \<in> d"
+ and "k2 \<in> d"
+ and "k1 \<noteq> k2"
+ and "k1 \<inter> {x::'a. x\<bullet>k \<le> c} = k2 \<inter> {x. x\<bullet>k \<le> c}"
+ and k: "k\<in>Basis"
shows "content(k1 \<inter> {x. x\<bullet>k \<le> c}) = 0"
-proof- note d=division_ofD[OF assms(1)]
- have *:"\<And>a b::'a. \<And> c. (content({a..b} \<inter> {x. x\<bullet>k \<le> c}) = 0 \<longleftrightarrow> interior({a..b} \<inter> {x. x\<bullet>k \<le> c}) = {})"
+proof -
+ note d=division_ofD[OF assms(1)]
+ have *: "\<And>a b::'a. \<And> c. (content({a..b} \<inter> {x. x\<bullet>k \<le> c}) = 0 \<longleftrightarrow> interior({a..b} \<inter> {x. x\<bullet>k \<le> 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 **:"\<And>s t u. s \<inter> t = {} \<Longrightarrow> u \<subseteq> s \<Longrightarrow> u \<subseteq> t \<Longrightarrow> 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 \<in> d" "k2 \<in> d" "k1 \<noteq> k2"
- "k1 \<inter> {x::'a. x\<bullet>k \<ge> c} = k2 \<inter> {x. x\<bullet>k \<ge> c}" and k:"k\<in>Basis"
- shows "content(k1 \<inter> {x. x\<bullet>k \<ge> c}) = 0"
-proof- note d=division_ofD[OF assms(1)]
- have *:"\<And>a b::'a. \<And> c. (content({a..b} \<inter> {x. x\<bullet>k >= c}) = 0 \<longleftrightarrow> interior({a..b} \<inter> {x. x\<bullet>k >= c}) = {})"
+ have **: "\<And>s t u. s \<inter> t = {} \<Longrightarrow> u \<subseteq> s \<Longrightarrow> u \<subseteq> t \<Longrightarrow> 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 \<in> d"
+ and "k2 \<in> d"
+ and "k1 \<noteq> k2"
+ and "k1 \<inter> {x::'a. x\<bullet>k \<ge> c} = k2 \<inter> {x. x\<bullet>k \<ge> c}"
+ and k: "k \<in> Basis"
+ shows "content (k1 \<inter> {x. x\<bullet>k \<ge> c}) = 0"
+proof -
+ note d=division_ofD[OF assms(1)]
+ have *: "\<And>a b::'a. \<And>c. content({a..b} \<inter> {x. x\<bullet>k \<ge> c}) = 0 \<longleftrightarrow>
+ interior({a..b} \<inter> {x. x\<bullet>k \<ge> 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 **:"\<And>s t u. s \<inter> t = {} \<Longrightarrow> u \<subseteq> s \<Longrightarrow> u \<subseteq> t \<Longrightarrow> 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) \<in> d" "(x2,k2) \<in> d" "k1 \<noteq> k2" "k1 \<inter> {x. x\<bullet>k \<le> c} = k2 \<inter> {x. x\<bullet>k \<le> c}"
- and k:"k\<in>Basis"
- shows "content(k1 \<inter> {x. x\<bullet>k \<le> c}) = 0"
-proof- have *:"\<And>a b c. (a,b) \<in> c \<Longrightarrow> b \<in> 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) \<in> d" "(x2,k2) \<in> d" "k1 \<noteq> k2" "k1 \<inter> {x. x\<bullet>k \<ge> c} = k2 \<inter> {x. x\<bullet>k \<ge> c}"
- and k:"k\<in>Basis"
+ have **: "\<And>s t u. s \<inter> t = {} \<Longrightarrow> u \<subseteq> s \<Longrightarrow> u \<subseteq> t \<Longrightarrow> 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) \<in> d"
+ and "(x2, k2) \<in> d"
+ and "k1 \<noteq> k2"
+ and "k1 \<inter> {x. x\<bullet>k \<le> c} = k2 \<inter> {x. x\<bullet>k \<le> c}"
+ and k: "k \<in> Basis"
+ shows "content (k1 \<inter> {x. x\<bullet>k \<le> c}) = 0"
+proof -
+ have *: "\<And>a b c. (a,b) \<in> c \<Longrightarrow> b \<in> 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) \<in> d"
+ and "(x2, k2) \<in> d"
+ and "k1 \<noteq> k2"
+ and "k1 \<inter> {x. x\<bullet>k \<ge> c} = k2 \<inter> {x. x\<bullet>k \<ge> c}"
+ and k: "k \<in> Basis"
shows "content(k1 \<inter> {x. x\<bullet>k \<ge> c}) = 0"
-proof- have *:"\<And>a b c. (a,b) \<in> c \<Longrightarrow> b \<in> 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 *: "\<And>a b c. (a,b) \<in> c \<Longrightarrow> b \<in> 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\<in>Basis"
--- 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("!<symlink>" + 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")
- }
-}
-
--- 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
}
--- /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
+ }
+}
+
--- 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)
+ }
}
}
--- 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
--- 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"),
+ """<DOCKING LEFT="" TOP="" RIGHT="" BOTTOM="isabelle-readme" LEFT_POS="0" TOP_POS="0" RIGHT_POS="250" BOTTOM_POS="250" />""")
+ File.write(settings_dir + Path.explode("perspective.xml"),
+ """<?xml version="1.0" encoding="UTF-8" ?>
+<!DOCTYPE PERSPECTIVE SYSTEM "perspective.dtd">
+<PERSPECTIVE>
+<VIEW PLAIN="FALSE">
+<GEOMETRY X="0" Y="35" WIDTH="1072" HEIGHT="787" EXT_STATE="0" />
+</VIEW>
+</PERSPECTIVE>""")
+ }
+
- 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("!<symlink>" + 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()
}
}
--- 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"
--- 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[@]}"
--- 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
-<DOCKING LEFT="" TOP="" RIGHT="" BOTTOM="isabelle-readme" LEFT_POS="0" TOP_POS="0" RIGHT_POS="250" BOTTOM_POS="250" />
-EOF
- cat > "$JEDIT_SETTINGS/perspective.xml" <<EOF
-<?xml version="1.0" encoding="UTF-8" ?>
-<!DOCTYPE PERSPECTIVE SYSTEM "perspective.dtd">
-<PERSPECTIVE>
-<VIEW PLAIN="FALSE">
-<GEOMETRY X="0" Y="35" WIDTH="1072" HEIGHT="787" EXT_STATE="0" />
-</VIEW>
-</PERSPECTIVE>
-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
--- 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)
- }
-}
-