--- a/Admin/Linux/Isabelle Thu Sep 12 17:36:06 2013 +0200
+++ b/Admin/Linux/Isabelle Thu Sep 12 20:54:26 2013 +0200
@@ -4,25 +4,24 @@
#
# Main Isabelle application wrapper.
+# dereference executable
if [ -L "$0" ]; then
TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
fi
-## settings
-
-PRG="$(basename "$0")"
+# minimal Isabelle environment
ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; pwd)"
-source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
+source "$ISABELLE_HOME/lib/scripts/isabelle-platform"
-## main
+# main
-declare -a JAVA_ARGS
-JAVA_ARGS=({JAVA_ARGS})
+exec "$ISABELLE_HOME/contrib/jdk/${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}/bin/java" \
+ "-Disabelle.home=$ISABELLE_HOME" \
+ {JAVA_ARGS} \
+ -classpath "{CLASSPATH}" \
+ isabelle.Main "$@"
-exec "$ISABELLE_HOME/bin/isabelle" java "${JAVA_ARGS[@]}" \
- -classpath "$ISABELLE_HOME/src/Tools/jEdit/dist/jedit.jar" isabelle.Main "$@"
-
--- a/Admin/Release/CHECKLIST Thu Sep 12 17:36:06 2013 +0200
+++ b/Admin/Release/CHECKLIST Thu Sep 12 20:54:26 2013 +0200
@@ -11,6 +11,8 @@
- test 'display_drafts' command;
+- test "#!/usr/bin/env isabelle_scala_script";
+
- check HTML header of library;
- check file positions within logic images (hyperlinks etc.);
--- a/Admin/Windows/WinRun4J/Isabelle.ini Thu Sep 12 17:36:06 2013 +0200
+++ b/Admin/Windows/WinRun4J/Isabelle.ini Thu Sep 12 20:54:26 2013 +0200
@@ -1,11 +1,4 @@
main.class=isabelle.Main
-classpath.1=lib\classes\ext\Pure.jar
-classpath.2=lib\classes\ext\scala-compiler.jar
-classpath.3=lib\classes\ext\scala-library.jar
-classpath.4=lib\classes\ext\scala-swing.jar
-classpath.5=lib\classes\ext\scala-actors.jar
-classpath.6=lib\classes\ext\scala-reflect.jar
-classpath.7=src\Tools\jEdit\dist\jedit.jar
vm.location=contrib\jdk\x86-cygwin\jre\bin\server\jvm.dll
splash.image=lib\logo\isabelle.bmp
vmarg.1=-Disabelle.home=%INI_DIR%
--- a/Admin/build Thu Sep 12 17:36:06 2013 +0200
+++ b/Admin/build Thu Sep 12 20:54:26 2013 +0200
@@ -74,7 +74,7 @@
## main
-#workaround for scalac
+#workaround for scalac 2.10.2
function stty() { :; }
export -f stty
--- a/Admin/components/components.sha1 Thu Sep 12 17:36:06 2013 +0200
+++ b/Admin/components/components.sha1 Thu Sep 12 20:54:26 2013 +0200
@@ -34,6 +34,7 @@
c85c0829b8170f25aa65ec6852f505ce2a50639b jedit_build-20130628.tar.gz
5de3e399be2507f684b49dfd13da45228214bbe4 jedit_build-20130905.tar.gz
87136818fd5528d97288f5b06bd30c787229eb0d jedit_build-20130910.tar.gz
+0bd2bc2d9a491ba5fc8dd99df27c04f11a72e8fa jfreechart-1.0.14-1.tar.gz
8122526f1fc362ddae1a328bdbc2152853186fee jfreechart-1.0.14.tar.gz
6c737137cc597fc920943783382e928ea79e3feb kodkodi-1.2.16.tar.gz
5f95c96bb99927f3a026050f85bd056f37a9189e kodkodi-1.5.2.tar.gz
@@ -59,6 +60,7 @@
e6a43b7b3b21295853bd2a63b27ea20bd6102f5f windows_app-20130906.tar.gz
8fe004aead867d4c82425afac481142bd3f01fb0 windows_app-20130908.tar.gz
d273abdc7387462f77a127fa43095eed78332b5c windows_app-20130909.tar.gz
+1c36a840320dfa9bac8af25fc289a4df5ea3eccb xz-java-1.2-1.tar.gz
2ae13aa17d0dc95ce254a52f1dba10929763a10d xz-java-1.2.tar.gz
4530a1aa6f4498ee3d78d6000fa71a3f63bd077f yices-1.0.28.tar.gz
12ae71acde43bd7bed1e005c43034b208c0cba4c z3-3.2.tar.gz
--- a/Admin/components/main Thu Sep 12 17:36:06 2013 +0200
+++ b/Admin/components/main Thu Sep 12 20:54:26 2013 +0200
@@ -5,10 +5,10 @@
Haskabelle-2013
jdk-7u25
jedit_build-20130910
-jfreechart-1.0.14
+jfreechart-1.0.14-1
kodkodi-1.5.2
polyml-5.5.0-3
scala-2.10.2
spass-3.8ds
z3-3.2
-xz-java-1.2
+xz-java-1.2-1
--- a/Admin/lib/Tools/makedist Thu Sep 12 17:36:06 2013 +0200
+++ b/Admin/lib/Tools/makedist Thu Sep 12 20:54:26 2013 +0200
@@ -168,6 +168,8 @@
find . "(" -name \*.thy -o -name \*.ML -o -name \*.scala ")" -perm +111 -print | xargs chmod -f -x
find . -print | xargs chmod -f u+rw
+export CLASSPATH="$ISABELLE_CLASSPATH"
+
./bin/isabelle env ISABELLE_SCALA_BUILD_OPTIONS="$ISABELLE_SCALA_BUILD_OPTIONS -optimise" \
./Admin/build all || fail "Failed to build distribution"
--- a/Admin/lib/Tools/makedist_bundle Thu Sep 12 17:36:06 2013 +0200
+++ b/Admin/lib/Tools/makedist_bundle Thu Sep 12 20:54:26 2013 +0200
@@ -51,6 +51,30 @@
tar -C "$TMP" -x -z -f "$ARCHIVE" || exit 2
+# distribution classpath (based on educated guesses)
+
+splitarray ":" "$ISABELLE_CLASSPATH"; CLASSPATH_ENTRIES=("${SPLITARRAY[@]}")
+declare -a DISTRIBITION_CLASSPATH=()
+
+for ENTRY in "${CLASSPATH_ENTRIES[@]}"
+do
+ ENTRY=$(echo "$ENTRY" | perl -n -e "
+ if (m,$ISABELLE_HOME/(.*)\$,) { print qq{\$1}; }
+ elsif (m,$USER_HOME/.isabelle/contrib/(.*)\$,) { print qq{contrib/\$1}; }
+ else { print; };
+ print qq{\n};")
+ DISTRIBITION_CLASSPATH["${#DISTRIBITION_CLASSPATH[@]}"]="$ENTRY"
+done
+
+DISTRIBITION_CLASSPATH["${#DISTRIBITION_CLASSPATH[@]}"]="src/Tools/jEdit/dist/jedit.jar"
+
+echo "classpath"
+for ENTRY in "${DISTRIBITION_CLASSPATH[@]}"
+do
+ echo " $ENTRY"
+done
+
+
# bundled components
init_component "$JEDIT_HOME"
@@ -128,9 +152,19 @@
case "$PLATFORM_FAMILY" in
linux)
purge_contrib '-name "x86*-darwin" -o -name "x86*-cygwin" -o -name "x86*-windows"'
+
+ LINUX_CLASSPATH=""
+ for ENTRY in "${DISTRIBITION_CLASSPATH[@]}"
+ do
+ if [ -z "$LINUX_CLASSPATH" ]; then
+ LINUX_CLASSPATH="\\\$ISABELLE_HOME/$ENTRY"
+ else
+ LINUX_CLASSPATH="$LINUX_CLASSPATH:\\\$ISABELLE_HOME/$ENTRY"
+ fi
+ done
cat "$ISABELLE_HOME/Admin/Linux/Isabelle" | \
- perl -p -e "s,{JAVA_ARGS},$JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS,g;" \
- > "$ISABELLE_TARGET/$ISABELLE_NAME"
+ perl -p > "$ISABELLE_TARGET/$ISABELLE_NAME" \
+ -e "s,{JAVA_ARGS},$JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS,g; s,{CLASSPATH},$LINUX_CLASSPATH,;"
chmod +x "$ISABELLE_TARGET/$ISABELLE_NAME"
;;
macos)
@@ -151,6 +185,7 @@
(
cat "$ISABELLE_HOME/Admin/Windows/WinRun4J/Isabelle.ini"
+
declare -a JAVA_ARGS=()
eval "JAVA_ARGS=($ISABELLE_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS)"
A=2
@@ -159,6 +194,14 @@
echo -e "vmarg.$A=$ARG\r"
A=$[ $A + 1 ]
done
+
+ A=1
+ for ENTRY in "${DISTRIBITION_CLASSPATH[@]}"
+ do
+ ENTRY=$(echo "$ENTRY" | perl -p -e 's,/,\\\\,g;')
+ echo -e "classpath.$A=$ENTRY\r"
+ A=$[ $A + 1 ]
+ done
) > "$ISABELLE_TARGET/${ISABELLE_NAME}.ini"
cp "$TMP/windows_app/Isabelle.exe" "$ISABELLE_TARGET/${ISABELLE_NAME}.exe"
@@ -233,11 +276,10 @@
cat "$APP_TEMPLATE/Info.plist-part2"
) | perl -p -e "s,{ISABELLE_NAME},${ISABELLE_NAME},g;" > "$APP/Contents/Info.plist"
- for NAME in Pure.jar scala-compiler.jar scala-library.jar scala-swing.jar scala-actors.jar scala-reflect.jar
+ for ENTRY in "${DISTRIBITION_CLASSPATH[@]}"
do
- ln -sf "../Resources/${ISABELLE_NAME}/lib/classes/ext/$NAME" "$APP/Contents/Java"
+ ln -sf "../Resources/${ISABELLE_NAME}/$ENTRY" "$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/etc/settings Thu Sep 12 17:36:06 2013 +0200
+++ b/etc/settings Thu Sep 12 20:54:26 2013 +0200
@@ -15,6 +15,13 @@
ISABELLE_JAVA_SYSTEM_OPTIONS="-Dfile.encoding=UTF-8 -server"
+classpath "$ISABELLE_HOME/lib/classes/Pure.jar"
+classpath "$ISABELLE_HOME/lib/classes/scala-library.jar"
+classpath "$ISABELLE_HOME/lib/classes/scala-swing.jar"
+classpath "$ISABELLE_HOME/lib/classes/scala-actors.jar"
+classpath "$ISABELLE_HOME/lib/classes/scala-compiler.jar"
+classpath "$ISABELLE_HOME/lib/classes/scala-reflect.jar"
+
###
### Interactive sessions (cf. isabelle tty)
--- a/lib/Tools/java Thu Sep 12 17:36:06 2013 +0200
+++ b/lib/Tools/java Thu Sep 12 20:54:26 2013 +0200
@@ -4,9 +4,11 @@
#
# DESCRIPTION: invoke Java within the Isabelle environment
-CLASSPATH="$(jvmpath "$CLASSPATH")"
+declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_JAVA_SYSTEM_OPTIONS)"
-declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_JAVA_SYSTEM_OPTIONS)"
+[ -n "$CLASSPATH" ] && classpath "$CLASSPATH"
+unset CLASSPATH
+
isabelle_jdk java "${JAVA_ARGS[@]}" \
- "-Djava.ext.dirs=$(jvmpath "$ISABELLE_JAVA_EXT:$ISABELLE_HOME/lib/classes/ext")" "$@"
+ -classpath "$(jvmpath "$ISABELLE_CLASSPATH")" "$@"
--- a/lib/Tools/scala Thu Sep 12 17:36:06 2013 +0200
+++ b/lib/Tools/scala Thu Sep 12 20:54:26 2013 +0200
@@ -6,6 +6,6 @@
isabelle_admin_build jars || exit $?
-CLASSPATH="$(jvmpath "$CLASSPATH")"
isabelle_scala scala -Dfile.encoding=UTF-8 \
- "-Djava.ext.dirs=$(jvmpath "$ISABELLE_JAVA_EXT:$ISABELLE_HOME/lib/classes/ext")" "$@"
+ -classpath "$(jvmpath "$ISABELLE_CLASSPATH")" "$@"
+
--- a/lib/Tools/scalac Thu Sep 12 17:36:06 2013 +0200
+++ b/lib/Tools/scalac Thu Sep 12 20:54:26 2013 +0200
@@ -6,7 +6,6 @@
isabelle_admin_build jars || exit $?
-CLASSPATH="$(jvmpath "$CLASSPATH")"
isabelle_scala scalac -Dfile.encoding=UTF-8 \
- "-Djava.ext.dirs=$(jvmpath "$ISABELLE_JAVA_EXT:$ISABELLE_HOME/lib/classes/ext")" "$@"
+ -classpath "$(jvmpath "$ISABELLE_CLASSPATH")" "$@"
--- a/lib/scripts/getsettings Thu Sep 12 17:36:06 2013 +0200
+++ b/lib/scripts/getsettings Thu Sep 12 20:54:26 2013 +0200
@@ -21,16 +21,20 @@
ISABELLE_HOME_WINDOWS="$(cygpath -w "$(dirname "$ISABELLE_HOME")")\\$(basename "$ISABELLE_HOME")"
ISABELLE_HOME="$(cygpath -u "$ISABELLE_HOME_WINDOWS")"
- CLASSPATH="$(cygpath -i -u -p "$CLASSPATH")"
function jvmpath() { cygpath -i -C UTF8 -w -p "$@"; }
CYGWIN_ROOT="$(jvmpath "/")"
+
+ ISABELLE_CLASSPATH="$(cygpath -i -u -p "$CLASSPATH")"
+ unset CLASSPATH
else
if [ -z "$USER_HOME" ]; then
USER_HOME="$HOME"
fi
function jvmpath() { echo "$@"; }
- CLASSPATH="$CLASSPATH"
+
+ ISABELLE_CLASSPATH="$CLASSPATH"
+ unset CLASSPATH
fi
export ISABELLE_HOME
@@ -122,18 +126,18 @@
function isabelle_admin_build () { return 0; }
fi
-#CLASSPATH convenience
+#classpath
function classpath ()
{
for X in "$@"
do
- if [ -z "$CLASSPATH" ]; then
- CLASSPATH="$X"
+ if [ -z "$ISABELLE_CLASSPATH" ]; then
+ ISABELLE_CLASSPATH="$X"
else
- CLASSPATH="$X:$CLASSPATH"
+ ISABELLE_CLASSPATH="$ISABELLE_CLASSPATH:$X"
fi
done
- export CLASSPATH
+ export ISABELLE_CLASSPATH
}
#arrays
--- a/src/Doc/System/Scala.thy Thu Sep 12 17:36:06 2013 +0200
+++ b/src/Doc/System/Scala.thy Thu Sep 12 20:54:26 2013 +0200
@@ -61,10 +61,10 @@
This allows to compile further Scala modules, depending on existing
Isabelle/Scala functionality. The resulting class or jar files can
- be added to the @{setting CLASSPATH} via the @{verbatim classpath}
- Bash function that is provided by the Isabelle process environment.
- Thus add-on components can register themselves in a modular manner,
- see also \secref{sec:components}.
+ be added to the Java classpath the @{verbatim classpath} Bash
+ function that is provided by the Isabelle process environment. Thus
+ add-on components can register themselves in a modular manner, see
+ also \secref{sec:components}.
Note that jEdit (\secref{sec:tool-jedit}) has its own mechanisms for
adding plugin components, which needs special attention since
--- a/src/HOL/Multivariate_Analysis/Fashoda.thy Thu Sep 12 17:36:06 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Fashoda.thy Thu Sep 12 20:54:26 2013 +0200
@@ -1,7 +1,8 @@
-(* Author: John Harrison
- Translation from HOL light: Robert Himmelmann, TU Muenchen *)
+(* Author: John Harrison
+ Author: Robert Himmelmann, TU Muenchen (translation from HOL light)
+*)
-header {* Fashoda meet theorem. *}
+header {* Fashoda meet theorem *}
theory Fashoda
imports Brouwer_Fixpoint Path_Connected Cartesian_Euclidean_Space
@@ -15,131 +16,312 @@
lemma axis_in_Basis: "a \<in> Basis \<Longrightarrow> axis i a \<in> Basis"
by (auto simp add: Basis_vec_def axis_eq_axis)
-subsection {*Fashoda meet theorem. *}
+
+subsection {* Fashoda meet theorem *}
-lemma infnorm_2: "infnorm (x::real^2) = max (abs(x$1)) (abs(x$2))"
- unfolding infnorm_cart UNIV_2 apply(rule cSup_eq) by auto
+lemma infnorm_2:
+ fixes x :: "real^2"
+ shows "infnorm x = max (abs (x$1)) (abs (x$2))"
+ unfolding infnorm_cart UNIV_2 by (rule cSup_eq) auto
-lemma infnorm_eq_1_2: "infnorm (x::real^2) = 1 \<longleftrightarrow>
- (abs(x$1) \<le> 1 \<and> abs(x$2) \<le> 1 \<and> (x$1 = -1 \<or> x$1 = 1 \<or> x$2 = -1 \<or> x$2 = 1))"
+lemma infnorm_eq_1_2:
+ fixes x :: "real^2"
+ shows "infnorm x = 1 \<longleftrightarrow>
+ abs (x$1) \<le> 1 \<and> abs (x$2) \<le> 1 \<and> (x$1 = -1 \<or> x$1 = 1 \<or> x$2 = -1 \<or> x$2 = 1)"
unfolding infnorm_2 by auto
-lemma infnorm_eq_1_imp: assumes "infnorm (x::real^2) = 1" shows "abs(x$1) \<le> 1" "abs(x$2) \<le> 1"
+lemma infnorm_eq_1_imp:
+ fixes x :: "real^2"
+ assumes "infnorm x = 1"
+ shows "abs (x$1) \<le> 1" and "abs (x$2) \<le> 1"
using assms unfolding infnorm_eq_1_2 by auto
-lemma fashoda_unit: fixes f g::"real \<Rightarrow> real^2"
- assumes "f ` {- 1..1} \<subseteq> {- 1..1}" "g ` {- 1..1} \<subseteq> {- 1..1}"
- "continuous_on {- 1..1} f" "continuous_on {- 1..1} g"
- "f (- 1)$1 = - 1" "f 1$1 = 1" "g (- 1) $2 = -1" "g 1 $2 = 1"
- shows "\<exists>s\<in>{- 1..1}. \<exists>t\<in>{- 1..1}. f s = g t" proof(rule ccontr)
- case goal1 note as = this[unfolded bex_simps,rule_format]
+lemma fashoda_unit:
+ fixes f g :: "real \<Rightarrow> real^2"
+ assumes "f ` {- 1..1} \<subseteq> {- 1..1}"
+ and "g ` {- 1..1} \<subseteq> {- 1..1}"
+ and "continuous_on {- 1..1} f"
+ and "continuous_on {- 1..1} g"
+ and "f (- 1)$1 = - 1"
+ and "f 1$1 = 1" "g (- 1) $2 = -1"
+ and "g 1 $2 = 1"
+ shows "\<exists>s\<in>{- 1..1}. \<exists>t\<in>{- 1..1}. f s = g t"
+proof (rule ccontr)
+ assume "\<not> ?thesis"
+ note as = this[unfolded bex_simps,rule_format]
def sqprojection \<equiv> "\<lambda>z::real^2. (inverse (infnorm z)) *\<^sub>R z"
- def negatex \<equiv> "\<lambda>x::real^2. (vector [-(x$1), x$2])::real^2"
- have lem1:"\<forall>z::real^2. infnorm(negatex z) = infnorm z"
+ def negatex \<equiv> "\<lambda>x::real^2. (vector [-(x$1), x$2])::real^2"
+ have lem1: "\<forall>z::real^2. infnorm (negatex z) = infnorm z"
unfolding negatex_def infnorm_2 vector_2 by auto
- have lem2:"\<forall>z. z\<noteq>0 \<longrightarrow> infnorm(sqprojection z) = 1" unfolding sqprojection_def
- unfolding infnorm_mul[unfolded scalar_mult_eq_scaleR] unfolding abs_inverse real_abs_infnorm
- apply(subst infnorm_eq_0[THEN sym]) by auto
- let ?F = "(\<lambda>w::real^2. (f \<circ> (\<lambda>x. x$1)) w - (g \<circ> (\<lambda>x. x$2)) w)"
- have *:"\<And>i. (\<lambda>x::real^2. x $ i) ` {- 1..1} = {- 1..1::real}"
- apply(rule set_eqI) unfolding image_iff Bex_def mem_interval_cart apply rule defer
- apply(rule_tac x="vec x" in exI) by auto
- { fix x assume "x \<in> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w) ` {- 1..1::real^2}"
+ have lem2: "\<forall>z. z \<noteq> 0 \<longrightarrow> infnorm (sqprojection z) = 1"
+ unfolding sqprojection_def
+ unfolding infnorm_mul[unfolded scalar_mult_eq_scaleR]
+ unfolding abs_inverse real_abs_infnorm
+ apply (subst infnorm_eq_0[THEN sym])
+ apply auto
+ done
+ let ?F = "\<lambda>w::real^2. (f \<circ> (\<lambda>x. x$1)) w - (g \<circ> (\<lambda>x. x$2)) w"
+ have *: "\<And>i. (\<lambda>x::real^2. x $ i) ` {- 1..1} = {- 1..1::real}"
+ apply (rule set_eqI)
+ unfolding image_iff Bex_def mem_interval_cart
+ apply rule
+ defer
+ apply (rule_tac x="vec x" in exI)
+ apply auto
+ done
+ {
+ fix x
+ assume "x \<in> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w) ` {- 1..1::real^2}"
then guess w unfolding image_iff .. note w = this
- hence "x \<noteq> 0" using as[of "w$1" "w$2"] unfolding mem_interval_cart by auto} note x0=this
- have 21:"\<And>i::2. i\<noteq>1 \<Longrightarrow> i=2" using UNIV_2 by auto
- have 1:"{- 1<..<1::real^2} \<noteq> {}" unfolding interval_eq_empty_cart by auto
- have 2:"continuous_on {- 1..1} (negatex \<circ> sqprojection \<circ> ?F)"
- apply(intro continuous_on_intros continuous_on_component)
- unfolding * apply(rule assms)+
- apply(subst sqprojection_def)
- apply(intro continuous_on_intros)
- apply(simp add: infnorm_eq_0 x0)
- apply(rule linear_continuous_on)
- proof-
- show "bounded_linear negatex" apply(rule bounded_linearI') unfolding vec_eq_iff proof(rule_tac[!] allI) fix i::2 and x y::"real^2" and c::real
- show "negatex (x + y) $ i = (negatex x + negatex y) $ i" "negatex (c *\<^sub>R x) $ i = (c *\<^sub>R negatex x) $ i"
- apply-apply(case_tac[!] "i\<noteq>1") prefer 3 apply(drule_tac[1-2] 21)
- unfolding negatex_def by(auto simp add:vector_2 ) qed
+ then have "x \<noteq> 0"
+ using as[of "w$1" "w$2"]
+ unfolding mem_interval_cart
+ by auto
+ } note x0 = this
+ have 21: "\<And>i::2. i \<noteq> 1 \<Longrightarrow> i = 2"
+ using UNIV_2 by auto
+ have 1: "{- 1<..<1::real^2} \<noteq> {}"
+ unfolding interval_eq_empty_cart by auto
+ have 2: "continuous_on {- 1..1} (negatex \<circ> sqprojection \<circ> ?F)"
+ apply (intro continuous_on_intros continuous_on_component)
+ unfolding *
+ apply (rule assms)+
+ apply (subst sqprojection_def)
+ apply (intro continuous_on_intros)
+ apply (simp add: infnorm_eq_0 x0)
+ apply (rule linear_continuous_on)
+ proof -
+ show "bounded_linear negatex"
+ apply (rule bounded_linearI')
+ unfolding vec_eq_iff
+ proof (rule_tac[!] allI)
+ fix i :: 2
+ fix x y :: "real^2"
+ fix c :: real
+ show "negatex (x + y) $ i =
+ (negatex x + negatex y) $ i" "negatex (c *\<^sub>R x) $ i = (c *\<^sub>R negatex x) $ i"
+ apply -
+ apply (case_tac[!] "i\<noteq>1")
+ prefer 3
+ apply (drule_tac[1-2] 21)
+ unfolding negatex_def
+ apply (auto simp add:vector_2)
+ done
+ qed
qed
- have 3:"(negatex \<circ> sqprojection \<circ> ?F) ` {- 1..1} \<subseteq> {- 1..1}" unfolding subset_eq apply rule proof-
- case goal1 then guess y unfolding image_iff .. note y=this have "?F y \<noteq> 0" apply(rule x0) using y(1) by auto
- hence *:"infnorm (sqprojection (?F y)) = 1" unfolding y o_def apply- by(rule lem2[rule_format])
- have "infnorm x = 1" unfolding *[THEN sym] y o_def by(rule lem1[rule_format])
- thus "x\<in>{- 1..1}" unfolding mem_interval_cart infnorm_2 apply- apply rule
- proof-case goal1 thus ?case apply(cases "i=1") defer apply(drule 21) by auto qed qed
- guess x apply(rule brouwer_weak[of "{- 1..1::real^2}" "negatex \<circ> sqprojection \<circ> ?F"])
- apply(rule compact_interval convex_interval)+ unfolding interior_closed_interval
- apply(rule 1 2 3)+ . note x=this
- have "?F x \<noteq> 0" apply(rule x0) using x(1) by auto
- hence *:"infnorm (sqprojection (?F x)) = 1" unfolding o_def by(rule lem2[rule_format])
- have nx:"infnorm x = 1" apply(subst x(2)[THEN sym]) unfolding *[THEN sym] o_def by(rule lem1[rule_format])
- have "\<forall>x i. x \<noteq> 0 \<longrightarrow> (0 < (sqprojection x)$i \<longleftrightarrow> 0 < x$i)" "\<forall>x i. x \<noteq> 0 \<longrightarrow> ((sqprojection x)$i < 0 \<longleftrightarrow> x$i < 0)"
- apply- apply(rule_tac[!] allI impI)+ proof- fix x::"real^2" and i::2 assume x:"x\<noteq>0"
- have "inverse (infnorm x) > 0" using x[unfolded infnorm_pos_lt[THEN sym]] by auto
- thus "(0 < sqprojection x $ i) = (0 < x $ i)" "(sqprojection x $ i < 0) = (x $ i < 0)"
+ have 3: "(negatex \<circ> sqprojection \<circ> ?F) ` {- 1..1} \<subseteq> {- 1..1}"
+ unfolding subset_eq
+ apply rule
+ proof -
+ case goal1
+ then guess y unfolding image_iff .. note y=this
+ have "?F y \<noteq> 0"
+ apply (rule x0)
+ using y(1)
+ apply auto
+ done
+ then have *: "infnorm (sqprojection (?F y)) = 1"
+ unfolding y o_def by - (rule lem2[rule_format])
+ have "infnorm x = 1"
+ unfolding *[THEN sym] y o_def by (rule lem1[rule_format])
+ then show "x \<in> {- 1..1}"
+ unfolding mem_interval_cart infnorm_2
+ apply -
+ apply rule
+ proof -
+ case goal1
+ then show ?case
+ apply (cases "i = 1")
+ defer
+ apply (drule 21)
+ apply auto
+ done
+ qed
+ qed
+ guess x
+ apply (rule brouwer_weak[of "{- 1..1::real^2}" "negatex \<circ> sqprojection \<circ> ?F"])
+ apply (rule compact_interval convex_interval)+ unfolding interior_closed_interval
+ apply (rule 1 2 3)+
+ done
+ note x=this
+ have "?F x \<noteq> 0"
+ apply (rule x0)
+ using x(1)
+ apply auto
+ done
+ then have *: "infnorm (sqprojection (?F x)) = 1"
+ unfolding o_def by (rule lem2[rule_format])
+ have nx: "infnorm x = 1"
+ apply (subst x(2)[THEN sym])
+ unfolding *[THEN sym] o_def
+ apply (rule lem1[rule_format])
+ done
+ have "\<forall>x i. x \<noteq> 0 \<longrightarrow> (0 < (sqprojection x)$i \<longleftrightarrow> 0 < x$i)"
+ and "\<forall>x i. x \<noteq> 0 \<longrightarrow> ((sqprojection x)$i < 0 \<longleftrightarrow> x$i < 0)"
+ apply -
+ apply (rule_tac[!] allI impI)+
+ proof -
+ fix x :: "real^2"
+ fix i :: 2
+ assume x: "x \<noteq> 0"
+ have "inverse (infnorm x) > 0"
+ using x[unfolded infnorm_pos_lt[THEN sym]] by auto
+ then show "(0 < sqprojection x $ i) = (0 < x $ i)"
+ and "(sqprojection x $ i < 0) = (x $ i < 0)"
unfolding sqprojection_def vector_component_simps vector_scaleR_component real_scaleR_def
- unfolding zero_less_mult_iff mult_less_0_iff by(auto simp add:field_simps) qed
+ unfolding zero_less_mult_iff mult_less_0_iff
+ by (auto simp add: field_simps)
+ qed
note lem3 = this[rule_format]
- have x1:"x $ 1 \<in> {- 1..1::real}" "x $ 2 \<in> {- 1..1::real}" using x(1) unfolding mem_interval_cart by auto
- hence nz:"f (x $ 1) - g (x $ 2) \<noteq> 0" unfolding right_minus_eq apply-apply(rule as) by auto
- have "x $ 1 = -1 \<or> x $ 1 = 1 \<or> x $ 2 = -1 \<or> x $ 2 = 1" using nx unfolding infnorm_eq_1_2 by auto
- thus False proof- fix P Q R S
- presume "P \<or> Q \<or> R \<or> S" "P\<Longrightarrow>False" "Q\<Longrightarrow>False" "R\<Longrightarrow>False" "S\<Longrightarrow>False" thus False by auto
- next assume as:"x$1 = 1"
- hence *:"f (x $ 1) $ 1 = 1" using assms(6) by auto
+ have x1: "x $ 1 \<in> {- 1..1::real}" "x $ 2 \<in> {- 1..1::real}"
+ using x(1) unfolding mem_interval_cart by auto
+ then have nz: "f (x $ 1) - g (x $ 2) \<noteq> 0"
+ unfolding right_minus_eq
+ apply -
+ apply (rule as)
+ apply auto
+ done
+ have "x $ 1 = -1 \<or> x $ 1 = 1 \<or> x $ 2 = -1 \<or> x $ 2 = 1"
+ using nx unfolding infnorm_eq_1_2 by auto
+ then show False
+ proof -
+ fix P Q R S
+ presume "P \<or> Q \<or> R \<or> S"
+ and "P \<Longrightarrow> False"
+ and "Q \<Longrightarrow> False"
+ and "R \<Longrightarrow> False"
+ and "S \<Longrightarrow> False"
+ then show False by auto
+ next
+ assume as: "x$1 = 1"
+ then have *: "f (x $ 1) $ 1 = 1"
+ using assms(6) by auto
have "sqprojection (f (x$1) - g (x$2)) $ 1 < 0"
using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=1]]
- unfolding as negatex_def vector_2 by auto moreover
- from x1 have "g (x $ 2) \<in> {- 1..1}" apply-apply(rule assms(2)[unfolded subset_eq,rule_format]) by auto
- ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval_cart
- apply(erule_tac x=1 in allE) by auto
- next assume as:"x$1 = -1"
- hence *:"f (x $ 1) $ 1 = - 1" using assms(5) by auto
+ unfolding as negatex_def vector_2
+ by auto
+ moreover
+ from x1 have "g (x $ 2) \<in> {- 1..1}"
+ apply -
+ apply (rule assms(2)[unfolded subset_eq,rule_format])
+ apply auto
+ done
+ ultimately show False
+ unfolding lem3[OF nz] vector_component_simps * mem_interval_cart
+ apply (erule_tac x=1 in allE)
+ apply auto
+ done
+ next
+ assume as: "x$1 = -1"
+ then have *: "f (x $ 1) $ 1 = - 1"
+ using assms(5) by auto
have "sqprojection (f (x$1) - g (x$2)) $ 1 > 0"
using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=1]]
- unfolding as negatex_def vector_2 by auto moreover
- from x1 have "g (x $ 2) \<in> {- 1..1}" apply-apply(rule assms(2)[unfolded subset_eq,rule_format]) by auto
- ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval_cart
- apply(erule_tac x=1 in allE) by auto
- next assume as:"x$2 = 1"
- hence *:"g (x $ 2) $ 2 = 1" using assms(8) by auto
+ unfolding as negatex_def vector_2
+ by auto
+ moreover
+ from x1 have "g (x $ 2) \<in> {- 1..1}"
+ apply -
+ apply (rule assms(2)[unfolded subset_eq,rule_format])
+ apply auto
+ done
+ ultimately show False
+ unfolding lem3[OF nz] vector_component_simps * mem_interval_cart
+ apply (erule_tac x=1 in allE)
+ apply auto
+ done
+ next
+ assume as: "x$2 = 1"
+ then have *: "g (x $ 2) $ 2 = 1"
+ using assms(8) by auto
have "sqprojection (f (x$1) - g (x$2)) $ 2 > 0"
using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=2]]
- unfolding as negatex_def vector_2 by auto moreover
- from x1 have "f (x $ 1) \<in> {- 1..1}" apply-apply(rule assms(1)[unfolded subset_eq,rule_format]) by auto
- ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval_cart
- apply(erule_tac x=2 in allE) by auto
- next assume as:"x$2 = -1"
- hence *:"g (x $ 2) $ 2 = - 1" using assms(7) by auto
+ unfolding as negatex_def vector_2
+ by auto
+ moreover
+ from x1 have "f (x $ 1) \<in> {- 1..1}"
+ apply -
+ apply (rule assms(1)[unfolded subset_eq,rule_format])
+ apply auto
+ done
+ ultimately show False
+ unfolding lem3[OF nz] vector_component_simps * mem_interval_cart
+ apply (erule_tac x=2 in allE)
+ apply auto
+ done
+ next
+ assume as: "x$2 = -1"
+ then have *: "g (x $ 2) $ 2 = - 1"
+ using assms(7) by auto
have "sqprojection (f (x$1) - g (x$2)) $ 2 < 0"
using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=2]]
- unfolding as negatex_def vector_2 by auto moreover
- from x1 have "f (x $ 1) \<in> {- 1..1}" apply-apply(rule assms(1)[unfolded subset_eq,rule_format]) by auto
- ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval_cart
- apply(erule_tac x=2 in allE) by auto qed(auto) qed
+ unfolding as negatex_def vector_2
+ by auto
+ moreover
+ from x1 have "f (x $ 1) \<in> {- 1..1}"
+ apply -
+ apply (rule assms(1)[unfolded subset_eq,rule_format])
+ apply auto
+ done
+ ultimately show False
+ unfolding lem3[OF nz] vector_component_simps * mem_interval_cart
+ apply (erule_tac x=2 in allE)
+ apply auto
+ done
+ qed auto
+qed
-lemma fashoda_unit_path: fixes f ::"real \<Rightarrow> real^2" and g ::"real \<Rightarrow> real^2"
- assumes "path f" "path g" "path_image f \<subseteq> {- 1..1}" "path_image g \<subseteq> {- 1..1}"
- "(pathstart f)$1 = -1" "(pathfinish f)$1 = 1" "(pathstart g)$2 = -1" "(pathfinish g)$2 = 1"
- obtains z where "z \<in> path_image f" "z \<in> path_image g" proof-
+lemma fashoda_unit_path:
+ fixes f g :: "real \<Rightarrow> real^2"
+ assumes "path f"
+ and "path g"
+ and "path_image f \<subseteq> {- 1..1}"
+ and "path_image g \<subseteq> {- 1..1}"
+ and "(pathstart f)$1 = -1"
+ and "(pathfinish f)$1 = 1"
+ and "(pathstart g)$2 = -1"
+ and "(pathfinish g)$2 = 1"
+ obtains z where "z \<in> path_image f" and "z \<in> path_image g"
+proof -
note assms=assms[unfolded path_def pathstart_def pathfinish_def path_image_def]
def iscale \<equiv> "\<lambda>z::real. inverse 2 *\<^sub>R (z + 1)"
- have isc:"iscale ` {- 1..1} \<subseteq> {0..1}" unfolding iscale_def by(auto)
- have "\<exists>s\<in>{- 1..1}. \<exists>t\<in>{- 1..1}. (f \<circ> iscale) s = (g \<circ> iscale) t" proof(rule fashoda_unit)
+ have isc: "iscale ` {- 1..1} \<subseteq> {0..1}"
+ unfolding iscale_def by auto
+ have "\<exists>s\<in>{- 1..1}. \<exists>t\<in>{- 1..1}. (f \<circ> iscale) s = (g \<circ> iscale) t"
+ proof (rule fashoda_unit)
show "(f \<circ> iscale) ` {- 1..1} \<subseteq> {- 1..1}" "(g \<circ> iscale) ` {- 1..1} \<subseteq> {- 1..1}"
using isc and assms(3-4) unfolding image_compose by auto
- have *:"continuous_on {- 1..1} iscale" unfolding iscale_def by(rule continuous_on_intros)+
+ have *: "continuous_on {- 1..1} iscale"
+ unfolding iscale_def by (rule continuous_on_intros)+
show "continuous_on {- 1..1} (f \<circ> iscale)" "continuous_on {- 1..1} (g \<circ> iscale)"
- apply-apply(rule_tac[!] continuous_on_compose[OF *]) apply(rule_tac[!] continuous_on_subset[OF _ isc])
- by(rule assms)+ have *:"(1 / 2) *\<^sub>R (1 + (1::real^1)) = 1" unfolding vec_eq_iff by auto
- show "(f \<circ> iscale) (- 1) $ 1 = - 1" "(f \<circ> iscale) 1 $ 1 = 1" "(g \<circ> iscale) (- 1) $ 2 = -1" "(g \<circ> iscale) 1 $ 2 = 1"
- unfolding o_def iscale_def using assms by(auto simp add:*) qed
+ apply -
+ apply (rule_tac[!] continuous_on_compose[OF *])
+ apply (rule_tac[!] continuous_on_subset[OF _ isc])
+ apply (rule assms)+
+ done
+ have *: "(1 / 2) *\<^sub>R (1 + (1::real^1)) = 1"
+ unfolding vec_eq_iff by auto
+ show "(f \<circ> iscale) (- 1) $ 1 = - 1"
+ and "(f \<circ> iscale) 1 $ 1 = 1"
+ and "(g \<circ> iscale) (- 1) $ 2 = -1"
+ and "(g \<circ> iscale) 1 $ 2 = 1"
+ unfolding o_def iscale_def
+ using assms
+ by (auto simp add: *)
+ qed
then guess s .. from this(2) guess t .. note st=this
- show thesis apply(rule_tac z="f (iscale s)" in that)
- using st `s\<in>{- 1..1}` unfolding o_def path_image_def image_iff apply-
- apply(rule_tac x="iscale s" in bexI) prefer 3 apply(rule_tac x="iscale t" in bexI)
- using isc[unfolded subset_eq, rule_format] by auto qed
+ show thesis
+ apply (rule_tac z="f (iscale s)" in that)
+ using st `s\<in>{- 1..1}`
+ unfolding o_def path_image_def image_iff
+ apply -
+ apply (rule_tac x="iscale s" in bexI)
+ prefer 3
+ apply (rule_tac x="iscale t" in bexI)
+ using isc[unfolded subset_eq, rule_format]
+ apply auto
+ done
+qed
lemma fashoda: fixes b::"real^2"
assumes "path f" "path g" "path_image f \<subseteq> {a..b}" "path_image g \<subseteq> {a..b}"
--- a/src/Pure/Isar/keyword.ML Thu Sep 12 17:36:06 2013 +0200
+++ b/src/Pure/Isar/keyword.ML Thu Sep 12 20:54:26 2013 +0200
@@ -23,6 +23,7 @@
val thy_script: T
val thy_goal: T
val qed: T
+ val qed_script: T
val qed_block: T
val qed_global: T
val prf_heading2: T
@@ -103,6 +104,7 @@
val thy_script = kind "thy_script";
val thy_goal = kind "thy_goal";
val qed = kind "qed";
+val qed_script = kind "qed_script";
val qed_block = kind "qed_block";
val qed_global = kind "qed_global";
val prf_heading2 = kind "prf_heading2";
@@ -121,7 +123,7 @@
val kinds =
[control, diag, thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
- thy_load, thy_decl, thy_script, thy_goal, qed, qed_block, qed_global,
+ thy_load, thy_decl, thy_script, thy_goal, qed, qed_script, qed_block, qed_global,
prf_heading2, prf_heading3, prf_heading4, prf_goal, prf_block, prf_open,
prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
@@ -242,7 +244,7 @@
thy_load, thy_decl, thy_script, thy_goal];
val is_proof = command_category
- [qed, qed_block, qed_global, prf_heading2, prf_heading3, prf_heading4,
+ [qed, qed_script, qed_block, qed_global, prf_heading2, prf_heading3, prf_heading4,
prf_goal, prf_block, prf_open, prf_close, prf_chain, prf_decl,
prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
@@ -252,7 +254,7 @@
val is_theory_goal = command_category [thy_goal];
val is_proof_goal = command_category [prf_goal, prf_asm_goal, prf_asm_goal_script];
-val is_qed = command_category [qed, qed_block];
+val is_qed = command_category [qed, qed_script, qed_block];
val is_qed_global = command_category [qed_global];
end;
--- a/src/Pure/Isar/keyword.scala Thu Sep 12 17:36:06 2013 +0200
+++ b/src/Pure/Isar/keyword.scala Thu Sep 12 20:54:26 2013 +0200
@@ -25,6 +25,7 @@
val THY_SCRIPT = "thy_script"
val THY_GOAL = "thy_goal"
val QED = "qed"
+ val QED_SCRIPT = "qed_script"
val QED_BLOCK = "qed_block"
val QED_GLOBAL = "qed_global"
val PRF_HEADING2 = "prf_heading2"
@@ -53,10 +54,12 @@
val theory1 = Set(THY_BEGIN, THY_END)
val theory2 = Set(THY_DECL, THY_GOAL)
val proof =
- Set(QED, QED_BLOCK, QED_GLOBAL, PRF_HEADING2, PRF_HEADING3, PRF_HEADING4, PRF_GOAL, PRF_BLOCK,
- PRF_OPEN, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT)
+ Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_HEADING2, PRF_HEADING3, PRF_HEADING4,
+ PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL,
+ PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT)
val proof1 =
- Set(QED, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN, PRF_DECL)
+ Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE,
+ PRF_CHAIN, PRF_DECL)
val proof2 = Set(PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT)
val improper = Set(THY_SCRIPT, PRF_SCRIPT)
}
--- a/src/Pure/Pure.thy Thu Sep 12 17:36:06 2013 +0200
+++ b/src/Pure/Pure.thy Thu Sep 12 20:54:26 2013 +0200
@@ -68,7 +68,8 @@
and "}" :: prf_close % "proof"
and "next" :: prf_block % "proof"
and "qed" :: qed_block % "proof"
- and "by" ".." "." "done" "sorry" :: "qed" % "proof"
+ and "by" ".." "." "sorry" :: "qed" % "proof"
+ and "done" :: "qed_script" % "proof"
and "oops" :: qed_global % "proof"
and "defer" "prefer" "apply" :: prf_script % "proof"
and "apply_end" :: prf_script % "proof" == ""
--- a/src/Pure/System/gui_setup.scala Thu Sep 12 17:36:06 2013 +0200
+++ b/src/Pure/System/gui_setup.scala Thu Sep 12 20:54:26 2013 +0200
@@ -44,7 +44,7 @@
// values
text.append("JVM name: " + Platform.jvm_name + "\n")
text.append("JVM platform: " + Platform.jvm_platform + "\n")
- text.append("JVM home: " + java.lang.System.getProperty("java.home") + "\n")
+ text.append("JVM home: " + java.lang.System.getProperty("java.home", "") + "\n")
try {
Isabelle_System.init()
if (Platform.is_windows)
--- a/src/Pure/System/isabelle_system.scala Thu Sep 12 17:36:06 2013 +0200
+++ b/src/Pure/System/isabelle_system.scala Thu Sep 12 20:54:26 2013 +0200
@@ -21,7 +21,7 @@
def jdk_home(): String =
{
- val java_home = System.getProperty("java.home")
+ val java_home = System.getProperty("java.home", "")
val home = new JFile(java_home)
val parent = home.getParent
if (home.getName == "jre" && parent != null &&
@@ -74,9 +74,9 @@
set_cygwin_root()
val env0 = sys.env + ("ISABELLE_JDK_HOME" -> posix_path(jdk_home()))
- val user_home = System.getProperty("user.home")
+ val user_home = System.getProperty("user.home", "")
val env =
- if (user_home == null || env0.isDefinedAt("HOME")) env0
+ if (user_home == "" || env0.isDefinedAt("HOME")) env0
else env0 + ("HOME" -> user_home)
val system_home =
@@ -84,8 +84,8 @@
else
env.get("ISABELLE_HOME") match {
case None | Some("") =>
- val path = System.getProperty("isabelle.home")
- if (path == null || path == "") error("Unknown Isabelle home directory")
+ val path = System.getProperty("isabelle.home", "")
+ if (path == "") error("Unknown Isabelle home directory")
else path
case Some(path) => path
}
--- a/src/Pure/System/platform.scala Thu Sep 12 17:36:06 2013 +0200
+++ b/src/Pure/System/platform.scala Thu Sep 12 20:54:26 2013 +0200
@@ -16,8 +16,8 @@
{
/* main OS variants */
- val is_macos = System.getProperty("os.name") == "Mac OS X"
- val is_windows = System.getProperty("os.name").startsWith("Windows")
+ val is_macos = System.getProperty("os.name", "") == "Mac OS X"
+ val is_windows = System.getProperty("os.name", "").startsWith("Windows")
/* Platform identifiers */
@@ -35,7 +35,7 @@
lazy val jvm_platform: String =
{
val arch =
- System.getProperty("os.arch") match {
+ System.getProperty("os.arch", "") match {
case X86() => "x86"
case X86_64() => "x86_64"
case Sparc() => "sparc"
@@ -43,7 +43,7 @@
case _ => error("Failed to determine CPU architecture")
}
val os =
- System.getProperty("os.name") match {
+ System.getProperty("os.name", "") match {
case Solaris() => "solaris"
case Linux() => "linux"
case Darwin() => "darwin"
@@ -56,6 +56,6 @@
/* JVM name */
- val jvm_name: String = System.getProperty("java.vm.name")
+ val jvm_name: String = System.getProperty("java.vm.name", "")
}
--- a/src/Pure/Tools/keywords.scala Thu Sep 12 17:36:06 2013 +0200
+++ b/src/Pure/Tools/keywords.scala Thu Sep 12 20:54:26 2013 +0200
@@ -27,6 +27,7 @@
"thy_decl" -> "theory-decl",
"thy_script" -> "theory-script",
"thy_goal" -> "theory-goal",
+ "qed_script" -> "qed",
"qed_block" -> "qed-block",
"qed_global" -> "qed-global",
"prf_heading2" -> "proof-heading",
--- a/src/Pure/build-jars Thu Sep 12 17:36:06 2013 +0200
+++ b/src/Pure/build-jars Thu Sep 12 20:54:26 2013 +0200
@@ -140,19 +140,10 @@
[ "$#" -ne 0 ] && usage
-## dependencies
-
-declare -a JFREECHART_JARS=()
-for NAME in $JFREECHART_JAR_NAMES
-do
- JFREECHART_JARS["${#JFREECHART_JARS[@]}"]="$JFREECHART_HOME/lib/$NAME"
-done
-
-
## build
TARGET_DIR="$ISABELLE_HOME/lib/classes"
-TARGET="$TARGET_DIR/ext/Pure.jar"
+TARGET="$TARGET_DIR/Pure.jar"
declare -a PIDE_SOURCES=()
declare -a PURE_SOURCES=()
@@ -203,14 +194,10 @@
SCALAC_OPTIONS="$ISABELLE_SCALA_BUILD_OPTIONS -d classes"
- JFXRT="$ISABELLE_JDK_HOME/jre/lib/jfxrt.jar"
-
(
- for X in "$JFXRT" "${JFREECHART_JARS[@]}" "$XZ_JAVA_HOME/lib/xz.jar" classes
- do
- CLASSPATH="$CLASSPATH:$X"
- done
- CLASSPATH="$(jvmpath "$CLASSPATH")"
+ classpath "$ISABELLE_JDK_HOME/jre/lib/jfxrt.jar"
+ classpath classes
+ export CLASSPATH="$(jvmpath "$ISABELLE_CLASSPATH")"
if [ "$TEST_PIDE" = true ]; then
isabelle_scala scalac $SCALAC_OPTIONS "${PIDE_SOURCES[@]}" || \
@@ -223,7 +210,7 @@
fi
) || exit "$?"
- mkdir -p "$TARGET_DIR/ext" || fail "Failed to create directory $TARGET_DIR/ext"
+ mkdir -p "$TARGET_DIR" || fail "Failed to create directory $TARGET_DIR"
pushd classes >/dev/null
@@ -238,13 +225,10 @@
cp "$SCALA_HOME/lib/scala-compiler.jar" \
"$SCALA_HOME/lib/scala-library.jar" \
- "$SCALA_HOME/lib/scala-swing.jar" "$TARGET_DIR/ext"
-
- [ -e "$SCALA_HOME/lib/scala-actors.jar" ] && \
- cp "$SCALA_HOME/lib/scala-actors.jar" "$TARGET_DIR/ext"
-
- [ -e "$SCALA_HOME/lib/scala-reflect.jar" ] && \
- cp "$SCALA_HOME/lib/scala-reflect.jar" "$TARGET_DIR/ext"
+ "$SCALA_HOME/lib/scala-swing.jar" \
+ "$SCALA_HOME/lib/scala-actors.jar" \
+ "$SCALA_HOME/lib/scala-reflect.jar" \
+ "$TARGET_DIR"
popd >/dev/null
--- a/src/Tools/Graphview/lib/Tools/graphview Thu Sep 12 17:36:06 2013 +0200
+++ b/src/Tools/Graphview/lib/Tools/graphview Thu Sep 12 20:54:26 2013 +0200
@@ -94,10 +94,10 @@
pushd "$GRAPHVIEW_HOME" >/dev/null || failed
-PURE_JAR="$ISABELLE_HOME/lib/classes/ext/Pure.jar"
+PURE_JAR="$ISABELLE_HOME/lib/classes/Pure.jar"
TARGET_DIR="$ISABELLE_HOME/lib/classes"
-TARGET="$TARGET_DIR/ext/Graphview.jar"
+TARGET="$TARGET_DIR/Graphview.jar"
declare -a UPDATED=()
@@ -139,12 +139,12 @@
rm -rf classes && mkdir classes
(
- #workaround for scalac
+ #workaround for scalac 2.10.2
function stty() { :; }
export -f stty
- CLASSPATH="$CLASSPATH:$PURE_JAR"
- CLASSPATH="$(jvmpath "$CLASSPATH")"
+ classpath "$PURE_JAR"
+ export CLASSPATH="$(jvmpath "$ISABELLE_CLASSPATH")"
exec "$SCALA_HOME/bin/scalac" $ISABELLE_SCALA_BUILD_OPTIONS -d classes "${SOURCES[@]}"
) || fail "Failed to compile sources"
--- a/src/Tools/jEdit/lib/Tools/jedit Thu Sep 12 17:36:06 2013 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Thu Sep 12 20:54:26 2013 +0200
@@ -198,8 +198,8 @@
fi
fi
-PURE_JAR="$ISABELLE_HOME/lib/classes/ext/Pure.jar"
-GRAPHVIEW_JAR="$ISABELLE_HOME/lib/classes/ext/Graphview.jar"
+PURE_JAR="$ISABELLE_HOME/lib/classes/Pure.jar"
+GRAPHVIEW_JAR="$ISABELLE_HOME/lib/classes/Graphview.jar"
pushd "$JEDIT_HOME" >/dev/null || failed
@@ -216,12 +216,6 @@
"$ISABELLE_JEDIT_BUILD_HOME/contrib/jsr305-2.0.0.jar"
)
-declare -a JFREECHART_JARS=()
-for NAME in $JFREECHART_JAR_NAMES
-do
- JFREECHART_JARS["${#JFREECHART_JARS[@]}"]="$JFREECHART_HOME/lib/$NAME"
-done
-
# target
@@ -238,8 +232,8 @@
else
if [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then
declare -a DEPS=(
- "$JEDIT_JAR" "${JEDIT_JARS[@]}" "${JFREECHART_JARS[@]}" "$XZ_JAVA_HOME/lib/xz.jar"
- "$PURE_JAR" "$GRAPHVIEW_JAR" "${SOURCES[@]}" "${RESOURCES[@]}"
+ "$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR" "$GRAPHVIEW_JAR"
+ "${SOURCES[@]}" "${RESOURCES[@]}"
)
elif [ -e "$ISABELLE_HOME/Admin/build" ]; then
declare -a DEPS=("$PURE_JAR" "$GRAPHVIEW_JAR" "${SOURCES[@]}" "${RESOURCES[@]}")
@@ -293,16 +287,15 @@
cp -p -R -f "${JEDIT_JARS[@]}" dist/jars/. || failed
(
- #workaround for scalac
+ #workaround for scalac 2.10.2
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"
+ for JAR in "$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR" "$GRAPHVIEW_JAR"
do
- CLASSPATH="$CLASSPATH:$JAR"
+ classpath "$JAR"
done
- CLASSPATH="$(jvmpath "$CLASSPATH")"
+ export CLASSPATH="$(jvmpath "$ISABELLE_CLASSPATH")"
exec "$SCALA_HOME/bin/scalac" $ISABELLE_SCALA_BUILD_OPTIONS -d dist/classes "${SOURCES[@]}"
) || fail "Failed to compile sources"
@@ -317,9 +310,9 @@
## main
-if [ "$BUILD_ONLY" = false ]; then
+if [ "$BUILD_ONLY" = false ]
+then
export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_PRINT_MODE JEDIT_BUILD_MODE
-
- exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" \
- -classpath "$(jvmpath "$JEDIT_HOME/dist/jedit.jar")" isabelle.Main "${ARGS[@]}"
+ classpath "$JEDIT_HOME/dist/jedit.jar"
+ exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Main "${ARGS[@]}"
fi
--- a/src/Tools/jEdit/src/rendering.scala Thu Sep 12 17:36:06 2013 +0200
+++ b/src/Tools/jEdit/src/rendering.scala Thu Sep 12 20:54:26 2013 +0200
@@ -75,6 +75,7 @@
Map[String, Byte](
Keyword.THY_END -> KEYWORD2,
Keyword.THY_SCRIPT -> LABEL,
+ Keyword.QED_SCRIPT -> DIGIT,
Keyword.PRF_SCRIPT -> DIGIT,
Keyword.PRF_ASM -> KEYWORD3,
Keyword.PRF_ASM_GOAL -> KEYWORD3,
--- a/src/Tools/jEdit/src/scala_console.scala Thu Sep 12 17:36:06 2013 +0200
+++ b/src/Tools/jEdit/src/scala_console.scala Thu Sep 12 20:54:26 2013 +0200
@@ -46,7 +46,14 @@
find_files(new JFile(start),
entry => entry.isFile && entry.getName.endsWith(".jar")).map(_.getAbsolutePath)
else Nil
- val path = find_jars(jEdit.getSettingsDirectory) ::: find_jars(jEdit.getJEditHome)
+
+ val initial_class_path =
+ Library.space_explode(JFile.pathSeparatorChar, System.getProperty("java.class.path", ""))
+
+ val path =
+ initial_class_path :::
+ find_jars(jEdit.getSettingsDirectory) :::
+ find_jars(jEdit.getJEditHome)
path.mkString(JFile.pathSeparator)
}