Bump isabelle to 2013, fixes bug 468344

Package-Manager: portage-2.2.1/cvs/Linux x86_64
Manifest-Sign-Key: 0x618E971F

6 files changed, 622 insertions, 6 deletions

diff --git a/sci-mathematics/isabelle/ChangeLog b/sci-mathematics/isabelle/ChangeLog
index e27701d55688..16ba9db3930e 100644
--- a/sci-mathematics/isabelle/ChangeLog
+++ b/sci-mathematics/isabelle/ChangeLog
@@ -1,6 +1,14 @@
 # ChangeLog for sci-mathematics/isabelle
 # Copyright 1999-2013 Gentoo Foundation; Distributed under the GPL v2
-# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/isabelle/ChangeLog,v 1.8 2013/05/03 14:53:49 jer Exp $
+# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/isabelle/ChangeLog,v 1.9 2013/08/31 09:24:13 gienah Exp $
+
+*isabelle-2013 (31 Aug 2013)
+
+  31 Aug 2013; Mark Wright <gienah@gentoo.org>
+  +files/isabelle-2013-HOL-Predicate_Compile_Examples.patch,
+  +files/isabelle-2013-classpath.patch,
+  +files/isabelle-2013-gentoo-settings.patch, +isabelle-2013.ebuild:
+  Bump isabelle to 2013, fixes bug 468344
 
   03 May 2013; Jeroen Roovers <jer@gentoo.org> metadata.xml:
   Fix XML.
diff --git a/sci-mathematics/isabelle/Manifest b/sci-mathematics/isabelle/Manifest
index 6d37328581bd..6c3caa4cb363 100644
--- a/sci-mathematics/isabelle/Manifest
+++ b/sci-mathematics/isabelle/Manifest
@@ -12,19 +12,26 @@ AUX isabelle-2012-libsha1.patch 508 SHA256 c07e99215d76f4b0aecfffd64981d670fb424
 AUX isabelle-2012-redundant-equations-in-function-definitions-error.patch 1319 SHA256 87d766c5140708710935bc4156fddb8901a80fa5462d22974290f85bc13b4038 SHA512 70697b4c5c367af64ff77c809618c735ad364665e63f69154dae95ff1079efca04c77b3e7595d2f378fa7c7b8b382a5ebf8edd27bafc85a264d57e98ec27f0b4 WHIRLPOOL de3ed96c6070a72b2bf7e266ef0ad0a66487dcf320fcdcb7aa725052b205b39141c7cb01df6bf6c373e850ea4bd1d87daf2e949bc303ecee16248736672b2272
 AUX isabelle-2012-reverse-line-editor-order.patch 423 SHA256 51a172b46baaaa269488801bad3d46ba4ccd0e3df35b2c15dc9b75592ceb843e SHA512 de9499e5c0d9bc22a72ef15320490fea7e71afbfe1ab6bc3a6a71a866eda2050833d47aadc7c0c7b106d4f0a28fa9a062ec2d9a6c15bf6c0eedd54274df20515 WHIRLPOOL 3a96e039df568ffd449dc0dc18a888d55a5b3db2940beb7f7e28628e0abdd3bd4132162abc7cac8c633f562cb2b18afb8a4e84cea26fa18f086488bfd3781a48
 AUX isabelle-2012-signal-handling.patch 457 SHA256 df6e274300a8ac440fa140c7bdb130c42191a45b40067bac46fcf8141861df6f SHA512 a505385c64ab1d4687543a1f12cfe0be6c50947161860b25a4abac3ef28219ee51f6f2c560ae5fa6894c2be191836c84ba3a0cf3cc6c65e9ca3a6c07aa8ba823 WHIRLPOOL 8151a64ea11a5d800aebb64d9e0d622aa428ef7e071d3d8ff90551855bd753f5c82e3af79bc09c95ca1e6cb3780e2aa8786031e71be1cd62072c5c4bbe81654f
+AUX isabelle-2013-HOL-Predicate_Compile_Examples.patch 3388 SHA256 690917da79d2c4db7055dbabcff0923a604674ac3b82616e596aeb128034b7fd SHA512 105b7067a9e9470ee8f54212cb8ec4ff50806a9c3b2468eae7972884267c27da33c0606850376f7d318f40dcddbc0305235f895c1409d88412d917c9c973fc0a WHIRLPOOL 7bbe4d3e254ea1b677189daf9bd7925e497dfd386df7466d2e81bd6e11ba46dfa8bcb3cd8b662baf479f8e0e58eb2f3feea6eecf54d88c064adba803a9f85893
+AUX isabelle-2013-classpath.patch 5309 SHA256 5b6fad7851876fd1e070e12b714688aad749f7e85d83665aa99abb5a74ad9233 SHA512 47874fd4570ffa865cca1069f2e5189d0765ecac0df65e19997ea50f6ebe2790ed9b588a3d4669c9abca4c67b3c160d4cf563171b20218c8729391cb82f2b197 WHIRLPOOL 3d6e8d8e87ff11ceae025cae987f7901f765b64f01e5fd7cbf7c06715b8758e9648c8066adc01ce91920aaf1526108db80f008b818ce85dbbb938888a45f521e
+AUX isabelle-2013-gentoo-settings.patch 600 SHA256 8b8a0bd49fa4bc58222906c6d0315b03a09144b5c419acb21c03bad4ee13cdfb SHA512 d9eee090f79f5d4a82cb478160f69ac107ba486925ca1e87ea3cfbc84c402155665b384803b9b78c52514568d90ba77a177abfdf004a4ca9c4080eb49879b0e2 WHIRLPOOL 2b132ae5c8a57b440ec11a70a25061251d1bfb6551627848df21bce907a10834f7889d277a3f5c6cb9928817142c8aa1f08be2b8b783f84c766a6c5309d79863
 DIST Isabelle2011-1.tar.gz 42239059 SHA256 48d77fe31a16b44f6015aa7953a60bdad8fcec9e60847630dc7b98c053edfc08 SHA512 213207951455395659a91b0bc6c8520c084cb6c75098c8f24c0800e41474c90c92aae86ffb99415142f6cf63d569556661ba350024fe458daa54a5cc9db372fd WHIRLPOOL 7e7868c3f464f507aceb8e1f648c04394fdd69746242179e66cfad64f927cf4d6aba41970428da5e45cce90a30bcee29bdc373d8a9e4943eb61cd97480d0a366
 DIST Isabelle2012-doc-src.tar.gz 2688496 SHA256 e18965fe0f7f89b286d4707e38201f1edbea81f6b26aed59d63a633c03fec097 SHA512 5aaea56eb67e535d745d63314278b6ee8469e6d3bbf4ce4d7b3f5e04b24557783b56d50d905a5ad69187c42f44407023c95a9bfb6faab125c21edff7638ff21d WHIRLPOOL 278b63a243950b1596376ee04cbfddb7a93c747e9f6ee66c5b069ca0dae4ca8d10bef43e03069b6186a19c703f71a585633fc47c3c1a15de3a886ff468232127
 DIST Isabelle2012.tar.gz 49529865 SHA256 b86f957dee221041f92c9d4ced4758d45b4950339743d0d58b1ea6061e2b53f0 SHA512 1346f563233eba10bc14f7d140706b8bfba8e832f7ee5887316c829926136af07d700914a925272d8adc1275b0bdd682540518957910c136a15bfc60d61285a0 WHIRLPOOL 23b764a1a0044a9525d058e95da318f4425fadf7660edc8ab8f35b248f98dcff0dba2e533ff18d8bf47ea164cec12a9648642749de2a49887bbe84ed4e71a68b
+DIST Isabelle2013.tar.gz 54638791 SHA256 2f2cda9939248bd4346ad7e074cb6b2cfad70708777491c6262a5ae670c8f83a SHA512 e03f9b747f678749a562c3de6100f4f4e010ace51b2eb13bcde0a63591eec0cb4e081f7fad9147d022fe787b56eac3f037ab3a296080fd70cc7d058ea961a789 WHIRLPOOL 5cbcbc93bd2ce4723034c3d95d4678b2de90c924601b795c5da378cb76f58275e5d5f47ce9120234a9ea36e43ab759ced843dca76942378abfa1fb7aff858a65
 DIST jedit_build-20120414.tar.gz 7509120 SHA256 3c5840fd01b87013b05a92742d41f66f655df6fe9edef1525c6722f92d8f3e41 SHA512 2e2f0db4964a041ba54382a9c787246e1d433e43167019c6ea8d4cf6beb84ce438c0bc559d2588229b0166c91bac603bed39abc45d5d4267020f55eaba1aaa0c WHIRLPOOL 40b883943bde312b4c7adc43607ba4759e5ebe22cab3c922c81393375f917af21d4a8dc068e5692ffcf7bdfb1e7fe3081358dc8e346d1942582bf79e249b0cbb
+DIST jedit_build-isabelle-component-20130104.tar.gz 10734679 SHA256 22a4880deb1054a548476b22662b42bfaf5394ceb07b30eba69be433bcea1074 SHA512 bacdb3ca73d48fe9ba71dd32cd68e98333831f205dd3ced69bb9344c5b167ba084662f1108690f371b4b64f6b786955a332bcd51a2dc21c2179fb1b4727430dd WHIRLPOOL fc97923e08202e117ca3112b69f74a9f4663a70f55fa051ac55e02c85be57423f762263cac2ded33d9c2f412736e4fa0937aa07df3f36b915e806959055a796b
+DIST jfreechart-isabelle-component-1.0.14.tar.gz 3443727 SHA256 c873ad6f07edbcceb5c76aac2e848c7d7f12c78c93c05f7e97c4b1fdba7c2df0 SHA512 c55ec01b215368f064de2f288f788960a256445adca5565c00aa9c0fab5732707a9e72bcdb3838676c80e735c520b9948855d7a32b9076bf35f1a279320ee72a WHIRLPOOL ba1a75e21525c302a3b755d814502dad60c540c2004dd894f60fdd6966766f85d71bbb45728ca220a4a7cff334de81db756fbb89e1059f32e248cabf0a7b97d6
 EBUILD isabelle-2011.1-r1.ebuild 8114 SHA256 914fc9aec131d739bde342e8fa821415b5d31763a874b30d7dfa7464ceef25fc SHA512 9a2fdcefe6f6b7f6dc6f83f66b3944f92d6f22ad7630144ef97e296488c3c7b0041078c3a599f292042a063e09882d88747f0c42b83317ac3de08cafc8d213c7 WHIRLPOOL 23f853a92750bdefa7e7e1a29a88b3ae66e28d7760fec71582fc42d793884ff0255721c0787cd76d6d3ee1d7fe0e63e54f91a44f7dcbf98ed5fd60b04380699c
 EBUILD isabelle-2011.1.ebuild 4036 SHA256 6063b32c39e50c42e81051197ce46a735bb16448c13b5ff1f8af5018f07b3020 SHA512 430524175bd5fbf4beb325a93ef746bf5df5c2beabc4b6d9536c1f7370e0c1babdd9bf00a617076a74ff892e5909ffe01f791a7121bdf3fb3cd817eb42f4bf66 WHIRLPOOL 3e3bcc27aa6ff8f4853fb142c0a4312bb7eeb908639a3fc826ae882a16fca60c03374387f4e06b19f4b079afb562d782d786c75c1c4a36c2cac2db47c0f04e18
 EBUILD isabelle-2012.ebuild 11011 SHA256 b8d6bc8147868b37c15789fdd250bbade275f3341b34166626de1552c717daad SHA512 b3194156a2379dc783d7e32a29bd60e02e7d043a5705e4e4d482f86fa22cb944f236ee5aa49257134468040c9edf01af889b86cb9f80bc631e14f400ab42eaa4 WHIRLPOOL 13bd0f7080dee3d97fb9ed1870e6f4fa68e82c8cf203d3993c336a402afca24f3fc6b16d96cd45915bb02348b5c17346f588734158762d78ab9290f8b3934759
-MISC ChangeLog 2797 SHA256 6ffb5b62474a8932f2b0e160562414cd4a271eb0560fdba0c642bc8a044c00db SHA512 e5a9b41cd9bb27dcc7b80483efbd81ccee953906bc972658a58ccce3c36d91597bf092eab4e640efb9c036daa47811c5c9588c1a848d07b8242e688df450ef23 WHIRLPOOL b1d3fc1c866c2b6311d4604f6e546ccfa584429867be09ca9b21b548f3bc15a905a6d2715efe84efd90d825daa6ee051349f151e65deae9ea4a77d3865d16552
+EBUILD isabelle-2013.ebuild 12418 SHA256 f8b59c07c8af4faa6c6ffa9d4b6b3a10eeb17824d7421bf5c1dd4d7377328576 SHA512 aa0fa1ef99d943030cdea7912af437fbd773378b46009ab73b41494167b349732e41a922a054af525391f178383a4f7cd356abcf22abd5c90abf0e9da6922437 WHIRLPOOL 8efc0028f3300746825a516efd47ae5f2539938975d7c08456ae9cbbdf523dea564603625816656598cfb85e867dfebd67646f7521df9d8eebfe7abe52ad1dad
+MISC ChangeLog 3090 SHA256 9de7ef129f7021e78557170af13adbc73ff02b83efd2b221cb8680ebbd9b839a SHA512 2b396449648b93793636c98b70341067ceb45c1c65dad81182feb974f10c499e72af5c037b98c7948baed40a2e6a5ca1346473c342032aed703d049b0f5c3806 WHIRLPOOL ff60b469d12ae036961c46c53915b5b551c060048349bbe3e46148e2b1203791cf1e76bf5f14a5b370545809286ed7a6eaf93c14ee81a029a7413d2fdd83e3ca
 MISC metadata.xml 2156 SHA256 cade1f090a62a67146e6ebce508a20436e2c883d62dbc5a260733a60f69bd43b SHA512 cade4e370f3adbf9a5ae9bc6a73adabbe36f3ccc707c47f6f4516f2f0604b26f34439cff170bf478b3d52f0c507d72d9eef8f69657d7de2fda1f70a8a96de137 WHIRLPOOL 2edf4ab8a07ba560d34e168a9fd618a6fc1f9946dd0f9b62a2d071d1f19546d5e15413f54658c898e1e71df0c110ea832529f95cf904b7333489734fdfd5749b
 -----BEGIN PGP SIGNATURE-----
-Version: GnuPG v2.0.19 (GNU/Linux)
+Version: GnuPG v2.0.20 (GNU/Linux)
 
-iEYEAREIAAYFAlGDz34ACgkQVWmRsqeSphMVtgCcDdWoH3Uyd+6oS0AWS6gHNcD2
-l14Anj0ZC39At4RSovaNZgkMVNthWllB
-=zKAO
+iF4EAREIAAYFAlIhtcoACgkQoBEVQmGOlx+1nQEAuOTaeGSFm+bWG2QQfdPqB880
+hpM7jusMjr2AAwVuYMoA/3ccXvlkWlCVAiSYhOXTxLTDpQ3Wxpq5OPifOnkgpvq9
+=CuGB
 -----END PGP SIGNATURE-----
diff --git a/sci-mathematics/isabelle/files/isabelle-2013-HOL-Predicate_Compile_Examples.patch b/sci-mathematics/isabelle/files/isabelle-2013-HOL-Predicate_Compile_Examples.patch
new file mode 100644
index 000000000000..bce7eec4417c
--- /dev/null
+++ b/sci-mathematics/isabelle/files/isabelle-2013-HOL-Predicate_Compile_Examples.patch
@@ -0,0 +1,82 @@
+--- Isabelle2013-orig/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	2013-02-13 00:31:10.000000000 +1100
++++ Isabelle2013/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	2013-08-31 14:37:02.015159000 +1000
+@@ -82,7 +82,7 @@
+ setup {* Context.theory_map (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals))) *}
+ 
+ lemma "\<lbrakk> hotel s; isinp s r g \<rbrakk> \<Longrightarrow> owns s r = Some g"
+-quickcheck[tester = prolog, iterations = 1, expect = counterexample]
++quickcheck[tester = prolog, iterations = 1]
+ oops
+ 
+ section {* Manual setup to find the counterexample *}
+@@ -110,7 +110,7 @@
+ 
+ lemma
+   "hotel s ==> feels_safe s r ==> isinp s r g ==> owns s r = Some g"
+-quickcheck[tester = prolog, iterations = 1, expect = counterexample]
++quickcheck[tester = prolog, iterations = 1]
+ oops
+ 
+ section {* Using a global limit for limiting the execution *} 
+@@ -146,7 +146,7 @@
+ 
+ lemma
+   "hotel s ==> feels_safe s r ==> isinp s r g ==> owns s r = Some g"
+-quickcheck[tester = prolog, iterations = 1, expect = counterexample]
++quickcheck[tester = prolog, iterations = 1]
+ oops
+ 
+ end
+\ No newline at end of file
+--- Isabelle2013-orig/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy	2013-02-13 00:31:10.000000000 +1100
++++ Isabelle2013/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy	2013-08-31 14:36:47.049851000 +1000
+@@ -33,7 +33,7 @@
+ 
+ lemma
+   "S\<^isub>1p w \<Longrightarrow> w = []"
+-quickcheck[tester = prolog, iterations=1, expect = counterexample]
++quickcheck[tester = prolog, iterations=1]
+ oops
+ 
+ definition "filter_a = filter (\<lambda>x. x = a)"
+@@ -67,7 +67,7 @@
+ 
+ theorem S\<^isub>1_sound:
+ "S\<^isub>1p w \<Longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
+-quickcheck[tester = prolog, iterations=1, expect = counterexample]
++quickcheck[tester = prolog, iterations=1]
+ oops
+ 
+ 
+@@ -91,7 +91,7 @@
+ 
+ theorem S\<^isub>2_sound:
+   "S\<^isub>2p w \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
+-quickcheck[tester = prolog, iterations=1, expect = counterexample]
++quickcheck[tester = prolog, iterations=1]
+ oops
+ 
+ inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where
+--- Isabelle2013-orig/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy	2013-02-13 00:31:10.000000000 +1100
++++ Isabelle2013/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy	2013-08-31 14:28:11.784390000 +1000
+@@ -92,7 +92,7 @@
+ 
+ lemma
+   "\<Gamma> \<turnstile> t : U \<Longrightarrow> t \<rightarrow>\<^sub>\<beta> t' \<Longrightarrow> \<Gamma> \<turnstile> t' : U"
+-quickcheck[tester = prolog, iterations = 1, expect = counterexample]
++quickcheck[tester = prolog, iterations = 1]
+ oops
+ 
+ text {* Verifying that the found counterexample really is one by means of a proof *}
+--- Isabelle2013-orig/src/HOL/Predicate_Compile_Examples/List_Examples.thy	2013-02-13 00:31:10.000000000 +1100
++++ Isabelle2013/src/HOL/Predicate_Compile_Examples/List_Examples.thy	2013-08-31 14:27:52.013962000 +1000
+@@ -21,7 +21,7 @@
+ lemma "(xs :: nat list) = ys @ ys --> rev xs = xs"
+ quickcheck[tester = random, iterations = 10000]
+ quickcheck[tester = smart_exhaustive, iterations = 1, expect = counterexample]
+-quickcheck[tester = prolog, expect = counterexample]
++quickcheck[tester = prolog]
+ oops
+ 
+ end
+\ No newline at end of file
diff --git a/sci-mathematics/isabelle/files/isabelle-2013-classpath.patch b/sci-mathematics/isabelle/files/isabelle-2013-classpath.patch
new file mode 100644
index 000000000000..47a125461f49
--- /dev/null
+++ b/sci-mathematics/isabelle/files/isabelle-2013-classpath.patch
@@ -0,0 +1,149 @@
+--- Isabelle2013-orig/lib/Tools/java	2013-02-13 00:31:02.000000000 +1100
++++ Isabelle2013/lib/Tools/java	2013-08-18 14:07:51.704133000 +1000
+@@ -6,5 +6,5 @@
+ 
+ CLASSPATH="$(jvmpath "$CLASSPATH")"
+ isabelle_jdk java -Dfile.encoding=UTF-8 -server \
+-  "-Djava.ext.dirs=$(jvmpath "$ISABELLE_JAVA_EXT:$ISABELLE_HOME/lib/classes/ext")" "$@"
++  "-Djava.ext.dirs=$(jvmpath "$ISABELLE_JAVA_EXT:$ISABELLE_HOME/lib/classes/ext:$(java-config -p scala | sed 's@\([^:]*\)/[^:]*:.*@\1@')")" "$@"
+ 
+--- Isabelle2013-orig/lib/Tools/scala	2013-02-13 00:31:02.000000000 +1100
++++ Isabelle2013/lib/Tools/scala	2013-08-18 14:07:00.795248000 +1000
+@@ -8,4 +8,4 @@
+ 
+ CLASSPATH="$(jvmpath "$CLASSPATH")"
+ isabelle_scala scala -Dfile.encoding=UTF-8 \
+-  "-Djava.ext.dirs=$(jvmpath "$ISABELLE_JAVA_EXT:$ISABELLE_HOME/lib/classes/ext")" "$@"
++  "-Djava.ext.dirs=$(jvmpath "$ISABELLE_JAVA_EXT:$ISABELLE_HOME/lib/classes/ext:$(java-config -p scala | sed 's@\([^:]*\)/[^:]*:.*@\1@')")" "$@"
+--- Isabelle2013-orig/lib/Tools/scalac	2013-02-13 00:31:02.000000000 +1100
++++ Isabelle2013/lib/Tools/scalac	2013-08-18 14:07:32.751448000 +1000
+@@ -8,5 +8,5 @@
+ 
+ CLASSPATH="$(jvmpath "$CLASSPATH")"
+ isabelle_scala scalac -Dfile.encoding=UTF-8 \
+-  "-Djava.ext.dirs=$(jvmpath "$ISABELLE_JAVA_EXT:$ISABELLE_HOME/lib/classes/ext")" "$@"
++  "-Djava.ext.dirs=$(jvmpath "$ISABELLE_JAVA_EXT:$ISABELLE_HOME/lib/classes/ext:$(java-config -p scala | sed 's@\([^:]*\)/[^:]*:.*@\1@')")" "$@"
+ 
+--- Isabelle2013-orig/src/Pure/build-jars	2013-02-13 00:31:15.000000000 +1100
++++ Isabelle2013/src/Pure/build-jars	2013-08-18 12:55:51.400924000 +1000
+@@ -133,7 +133,7 @@
+ declare -a JFREECHART_JARS=()
+ for NAME in $JFREECHART_JAR_NAMES
+ do
+-  JFREECHART_JARS["${#JFREECHART_JARS[@]}"]="$JFREECHART_HOME/lib/$NAME"
++  JFREECHART_JARS["${#JFREECHART_JARS[@]}"]="$NAME"
+ done
+ 
+ 
+--- Isabelle2013-orig/src/Tools/jEdit/lib/Tools/jedit	2013-02-13 00:31:16.000000000 +1100
++++ Isabelle2013/src/Tools/jEdit/lib/Tools/jedit	2013-08-18 16:39:15.495244000 +1000
+@@ -214,97 +214,11 @@
+ declare -a JFREECHART_JARS=()
+ for NAME in $JFREECHART_JAR_NAMES
+ do
+-  JFREECHART_JARS["${#JFREECHART_JARS[@]}"]="$JFREECHART_HOME/lib/$NAME"
++  JFREECHART_JARS["${#JFREECHART_JARS[@]}"]="$NAME"
+ done
+ 
+-
+-# target
+-
+-TARGET="dist/jars/Isabelle-jEdit.jar"
+-
+-declare -a UPDATED=()
+-
+-if [ "$BUILD_JARS" = jars_fresh ]; then
+-  OUTDATED=true
+-else
+-  OUTDATED=false
+-  if [ ! -e "$TARGET" ]; then
+-    OUTDATED=true
+-  else
+-    if [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then
+-      declare -a DEPS=(
+-        "$JEDIT_JAR" "${JEDIT_JARS[@]}" "${JFREECHART_JARS[@]}"
+-        "$PURE_JAR" "$GRAPHVIEW_JAR" "${SOURCES[@]}" "${RESOURCES[@]}"
+-      )
+-    elif [ -e "$ISABELLE_HOME/Admin/build" ]; then
+-      declare -a DEPS=("$PURE_JAR" "$GRAPHVIEW_JAR" "${SOURCES[@]}" "${RESOURCES[@]}")
+-    else
+-      declare -a DEPS=()
+-    fi
+-    for DEP in "${DEPS[@]}"
+-    do
+-      [ ! -e "$DEP" ] && fail "Missing file: $DEP"
+-      [ "$DEP" -nt "$TARGET" ] && {
+-        OUTDATED=true
+-        UPDATED["${#UPDATED[@]}"]="$DEP"
+-      }
+-    done
+-  fi
+-fi
+-
+-
+-# build
+-
+-if [ "$OUTDATED" = true ]
+-then
+-  echo "### Building Isabelle/jEdit ..."
+-
+-  [ "${#UPDATED[@]}" -gt 0 ] && {
+-    echo "Changed files:"
+-    for FILE in "${UPDATED[@]}"
+-    do
+-      echo "  $FILE"
+-    done
+-  }
+-
+-  [ -z "$ISABELLE_JEDIT_BUILD_HOME" ] && \
+-    fail "Unknown ISABELLE_JEDIT_BUILD_HOME -- missing auxiliary component"
+-
+-  rm -rf dist || failed
+-  mkdir -p dist dist/classes || failed
+-
+-  cp -p -R -f "$ISABELLE_JEDIT_BUILD_HOME/contrib/$ISABELLE_JEDIT_BUILD_VERSION/." dist/.
+-  cp -p -R -f "${RESOURCES[@]}" dist/classes/.
+-  cp src/jEdit.props dist/properties/.
+-  cp -p -R -f src/modes/. dist/modes/.
+-
+-  perl -i -e 'while (<>) {
+-    if (m/NAME="javacc"/) {
+-      print qq,<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy"/>\n\n,;
+-      print qq,<MODE NAME="isabelle-options" FILE="isabelle-options.xml"/>\n\n,;
+-      print qq,<MODE NAME="isabelle-root" FILE="isabelle-root.xml" FILE_NAME_GLOB="ROOT"/>\n\n,; }
+-    print; }' dist/modes/catalog
+-
+-  cp -p -R -f "${JEDIT_JARS[@]}" dist/jars/. || failed
+-  (
+-    for JAR in "$JEDIT_JAR" "${JEDIT_JARS[@]}" "${JFREECHART_JARS[@]}" "$PURE_JAR" \
+-      "$GRAPHVIEW_JAR" "$SCALA_HOME/lib/scala-compiler.jar"
+-    do
+-      CLASSPATH="$CLASSPATH:$JAR"
+-    done
+-    CLASSPATH="$(jvmpath "$CLASSPATH")"
+-    exec "$SCALA_HOME/bin/scalac" $ISABELLE_SCALA_BUILD_OPTIONS -d dist/classes "${SOURCES[@]}"
+-  ) || fail "Failed to compile sources"
+-
+-  cd dist/classes
+-  isabelle_jdk jar cf "../jars/Isabelle-jEdit.jar" * || failed
+-  cd ../..
+-  rm -rf dist/classes
+-fi
+-
+ popd >/dev/null
+ 
+-
+ ## main
+ 
+ if [ "$BUILD_ONLY" = false ]; then
+--- Isabelle2013-orig/contrib/jfreechart-1.0.14/etc/settings	2012-12-09 07:23:53.000000000 +1100
++++ Isabelle2013/contrib/jfreechart-1.0.14/etc/settings	2013-08-18 16:18:10.244698000 +1000
+@@ -1,7 +1,5 @@
+ # -*- shell-script -*- :mode=shellscript:
+ 
+ JFREECHART_HOME="$COMPONENT"
+-JFREECHART_JAR_NAMES="iText-2.1.5.jar jcommon-1.0.18.jar jfreechart-1.0.14.jar"
+-
+-ISABELLE_JAVA_EXT="$ISABELLE_JAVA_EXT:$JFREECHART_HOME/lib"
++JFREECHART_JAR_NAMES="$(java-config -p itext | sed -e 's@:@ @g') $(java-config -p jcommon-1.0 | sed -e 's@:@ @g') $(java-config -p jfreechart-1.0 | sed -e 's@:@ @g')"
+ 
diff --git a/sci-mathematics/isabelle/files/isabelle-2013-gentoo-settings.patch b/sci-mathematics/isabelle/files/isabelle-2013-gentoo-settings.patch
new file mode 100644
index 000000000000..7066c6b875a2
--- /dev/null
+++ b/sci-mathematics/isabelle/files/isabelle-2013-gentoo-settings.patch
@@ -0,0 +1,19 @@
+--- Isabelle2013-orig/etc/settings	2013-02-13 00:31:02.000000000 +1100
++++ Isabelle2013/etc/settings	2013-08-17 14:47:46.045988000 +1000
+@@ -176,3 +176,16 @@
+ #ISABELLE_GHC="/usr/bin/ghc"
+ #ISABELLE_OCAML="/usr/bin/ocaml"
+ #ISABELLE_SWIPL="/usr/bin/swipl"
++
++# Poly/ML Gentoo (x86_64)
++ML_PLATFORM=x86_64-linux
++ML_HOME="/usr/bin"
++ML_SYSTEM=polyml-5.5.0
++ML_OPTIONS="-H 1000"
++ML_SOURCES="/usr/src/debug/dev-lang/polyml-5.5.0"
++
++# Proof General home
++PROOFGENERAL_HOME="/usr/share/emacs/site-lisp/ProofGeneral"
++PROOFGENERAL_OPTIONS=""
++#PROOFGENERAL_OPTIONS="-m no_brackets -m no_type_brackets"
++
diff --git a/sci-mathematics/isabelle/isabelle-2013.ebuild b/sci-mathematics/isabelle/isabelle-2013.ebuild
new file mode 100644
index 000000000000..37b0725375b7
--- /dev/null
+++ b/sci-mathematics/isabelle/isabelle-2013.ebuild
@@ -0,0 +1,351 @@
+# Copyright 1999-2013 Gentoo Foundation
+# Distributed under the terms of the GNU General Public License v2
+# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/isabelle/isabelle-2013.ebuild,v 1.1 2013/08/31 09:24:13 gienah Exp $
+
+EAPI="5"
+
+inherit eutils java-pkg-2 multilib versionator
+
+MY_PN="Isabelle"
+MY_PV=$(replace_all_version_separators '-')
+MY_P="${MY_PN}${MY_PV}"
+
+JEDIT_PV="20130104"
+JEDIT_PN="jedit_build"
+JEDIT_P="${JEDIT_PN}-${JEDIT_PV}"
+JEDIT_IC_PN="${JEDIT_PN}-isabelle-component"
+JEDIT_IC_P="${JEDIT_IC_PN}-${JEDIT_PV}"
+
+JFREECHART_PV="1.0.14"
+JFREECHART_PN="jfreechart"
+JFREECHART_P="${JFREECHART_PN}-${JFREECHART_PV}"
+JFREECHART_IC_PN="${JFREECHART_PN}-isabelle-component"
+JFREECHART_IC_P="${JFREECHART_IC_PN}-${JFREECHART_PV}"
+
+DESCRIPTION="Isabelle is a generic proof assistant"
+HOMEPAGE="http://www.cl.cam.ac.uk/research/hvg/isabelle/index.html"
+SRC_URI="http://www.cl.cam.ac.uk/research/hvg/isabelle/dist/${MY_P}.tar.gz
+		http://isabelle.in.tum.de/components/${JEDIT_P}.tar.gz -> ${JEDIT_IC_P}.tar.gz
+		http://isabelle.in.tum.de/components/${JFREECHART_P}.tar.gz -> ${JFREECHART_IC_P}.tar.gz"
+
+LICENSE="BSD"
+SLOT="0/${PV}"
+KEYWORDS="~amd64 ~x86"
+IUSE="doc graphbrowsing ledit readline proofgeneral"
+
+#upstream says
+#bash 2.x/3.x, Poly/ML 5.x, Perl 5.x,
+#for document preparation: complete LaTeX
+DEPEND=">=app-shells/bash-3.0
+	dev-java/ant-core
+	>=dev-java/jcommon-1.0.18
+	>=dev-java/jfreechart-1.0.14
+	>=dev-java/itext-2.1.5
+	dev-java/xml-xmlbeans:1
+	>=dev-lang/ghc-7.6.3
+	>=dev-lang/polyml-5.5.0:=[-portable]
+	>=dev-lang/perl-5.8.8-r2
+	dev-lang/swi-prolog
+	virtual/jdk:1.7
+	doc? (
+		virtual/latex-base
+		dev-tex/rail
+	)
+	>=dev-lang/scala-2.10.2
+	ledit? (
+		app-misc/ledit
+	)
+	readline? (
+		app-misc/rlwrap
+	)"
+
+RDEPEND="dev-perl/libwww-perl
+	sci-mathematics/sha1-polyml
+	>=virtual/jre-1.7
+	proofgeneral? (
+		>=app-emacs/proofgeneral-4.1
+	)
+	${DEPEND}"
+
+S="${WORKDIR}"/Isabelle${MY_PV}
+JEDIT_S="${WORKDIR}/${JEDIT_P}"
+JFREECHART_S="${WORKDIR}/${JFREECHART_P}"
+TARGETDIR="/usr/share/Isabelle"${MY_PV}
+LIBDIR="/usr/"$(get_libdir)"/Isabelle"${MY_PV}
+
+LIBRARY_PKGS="scala,itext,jcommon-1.0,jfreechart-1.0,xml-xmlbeans-1"
+
+src_unpack() {
+	unpack "${MY_P}.tar.gz"
+	pushd "${S}/contrib" || die
+	unpack ${JEDIT_IC_P}.tar.gz
+	unpack ${JFREECHART_IC_P}.tar.gz
+}
+
+pkg_setup() {
+	java-pkg-2_pkg_setup
+}
+
+src_prepare() {
+	java-pkg-2_src_prepare
+	java-pkg_getjars ${LIBRARY_PKGS}
+	epatch "${FILESDIR}/${PN}-2013-gentoo-settings.patch"
+	epatch "${FILESDIR}/${PN}-2013-classpath.patch"
+	polymlver=$(poly -v | cut -d' ' -f2)
+	polymlarch=$(poly -v | cut -d' ' -f9 | cut -d'-' -f1)
+	sed -e "s@5.5.0@${polymlver}@g" \
+		-i "${S}/etc/settings" \
+		|| die "Could not configure polyml version in etc/settings"
+	sed -e "s@ML_HOME=\"/@ML_HOME=\"${ROOT}@" \
+		-i "${S}/etc/settings" \
+		|| die "Could not configure polyml ML_HOME in etc/settings"
+	sed -e "s@x86_64@${polymlarch}@g" \
+		-i "${S}/etc/settings" \
+		|| die "Could not configure polyml arch in etc/settings"
+	sed -e "s@PROOFGENERAL_HOME=\"/@PROOFGENERAL_HOME=\"${ROOT}@" \
+		-i "${S}/etc/settings" \
+		|| die "Could not configure PROOFGENERAL_HOME in etc/settings"
+	sed -e "s@/usr/lib64/Isabelle${MY_PV}@${LIBDIR}@g" \
+		-i "${S}/etc/settings" \
+		|| die "Could not configure Isabelle lib directory in etc/settings"
+	epatch "${FILESDIR}/${PN}-2012-graphbrowser.patch"
+	epatch "${FILESDIR}/${PN}-2012-libsha1.patch"
+	# this example fails to compile with swi-prolog 6.5.2, so patch it so that
+	# Isabelle will build, then reverse the patch so that the user can see the
+	# original code.
+	epatch "${FILESDIR}/${PN}-2013-HOL-Predicate_Compile_Examples.patch"
+	cat <<- EOF >> "${S}/etc/settings"
+
+		ISABELLE_GHC="${ROOT}usr/bin/ghc"
+		ISABELLE_OCAML="${ROOT}usr/bin/ocaml"
+		ISABELLE_SWIPL="${ROOT}usr/bin/swipl"
+		ISABELLE_JDK_HOME="\$(java-config --jdk-home)"
+		SCALA_HOME="${ROOT}usr/share/scala"
+		SHA1_HOME="/usr/$(get_libdir)/sha1-polyml"
+	EOF
+	cat <<- EOF >> "${S}/etc/components"
+		#bundled components
+		contrib/${JEDIT_P}
+		contrib/${JFREECHART_P}
+	EOF
+	if use ledit && !use readline; then
+		epatch "${FILESDIR}/${PN}-2012-reverse-line-editor-order.patch"
+	fi
+	rm -f "${S}/contrib/jfreechart-1.0.14/lib/iText-2.1.5.jar" \
+		"${S}/contrib/jfreechart-1.0.14/lib/jfreechart-1.0.14.jar" \
+		"${S}/contrib/jfreechart-1.0.14/lib/jcommon-1.0.18.jar" \
+		"${S}/lib/classes/ext/scala-actors.jar" \
+		"${S}/lib/classes/ext/scala-compiler.jar" \
+		"${S}/lib/classes/ext/scala-library.jar" \
+		"${S}/lib/classes/ext/scala-reflect.jar" \
+		"${S}/lib/classes/ext/scala-swing.jar" \
+		|| die "Could not rm bundled jar files supplied by Gentoo"
+}
+
+src_compile() {
+	einfo "Building Isabelle. This may take some time."
+	./bin/isabelle build -a -b -s -v || die "isabelle build failed"
+	epatch --reverse "${FILESDIR}/${PN}-2013-HOL-Predicate_Compile_Examples.patch"
+	if use graphbrowsing
+	then
+		rm -f "${S}/lib/browser/GraphBrowser.jar" \
+			|| die "failed cleaning graph browser directory"
+		pushd "${S}/lib/browser" \
+			|| die "Could not change directory to lib/browser"
+		./build || die "failed building the graph browser"
+		popd
+	fi
+	./bin/isabelle jedit -b -f || die "pide build failed"
+}
+
+src_install() {
+	exeinto ${TARGETDIR}/bin
+	doexe bin/isabelle-process bin/isabelle
+
+	insinto ${TARGETDIR}
+	doins -r src
+	doins -r lib
+	doins -r contrib
+	doins ROOTS
+
+	docompress -x /usr/share/doc/${PF}
+	dodoc -r doc
+	if use doc; then
+		dosym /usr/share/doc/${PF}/doc "${TARGETDIR}/doc"
+		# The build of sci-mathematics/haskabelle with use doc requires
+		# sci-mathematics/isabelle[doc?]. The haskabelle doc build requires
+		# the src/Doc directory stuff in the isabelle package.
+		doins -r src/Doc
+		for i in "./src/Doc/Classes/document/build" \
+		"./src/Doc/Codegen/document/build" \
+		"./src/Doc/Functions/document/build" \
+		"./src/Doc/HOL/document/build" \
+		"./src/Doc/Intro/document/build" \
+		"./src/Doc/IsarImplementation/document/build" \
+		"./src/Doc/IsarRef/document/build" \
+		"./src/Doc/IsarRef/document/showsymbols" \
+		"./src/Doc/LaTeXsugar/document/build" \
+		"./src/Doc/Locales/document/build" \
+		"./src/Doc/Logics/document/build" \
+		"./src/Doc/Main/document/build" \
+		"./src/Doc/Nitpick/document/build" \
+		"./src/Doc/ProgProve/document/build" \
+		"./src/Doc/Ref/document/build" \
+		"./src/Doc/Sledgehammer/document/build" \
+		"./src/Doc/System/document/build" \
+		"./src/Doc/Tutorial/document/build" \
+		"./src/Doc/Tutorial/document/isa-index" \
+		"./src/Doc/ZF/document/build" \
+		"./src/Doc/fixbookmarks" \
+		"./src/Doc/prepare_document" \
+		"./src/Doc/sedindex"
+		do
+			exeinto $(dirname "${TARGETDIR}/${i}")
+			doexe ${i}
+		done
+	fi
+
+	for i in "./Isabelle " \
+		"./bin/isabelle" \
+		"./bin/isabelle-process" \
+		"./lib/Tools/browser" \
+		"./lib/Tools/build" \
+		"./lib/Tools/build_dialog" \
+		"./lib/Tools/components" \
+		"./lib/Tools/dimacs2hol" \
+		"./lib/Tools/display" \
+		"./lib/Tools/doc" \
+		"./lib/Tools/document" \
+		"./lib/Tools/emacs" \
+		"./lib/Tools/env" \
+		"./lib/Tools/findlogics" \
+		"./lib/Tools/getenv" \
+		"./lib/Tools/install" \
+		"./lib/Tools/java" \
+		"./lib/Tools/keywords" \
+		"./lib/Tools/latex" \
+		"./lib/Tools/logo" \
+		"./lib/Tools/make" \
+		"./lib/Tools/mkdir" \
+		"./lib/Tools/mkproject" \
+		"./lib/Tools/mkroot" \
+		"./lib/Tools/options" \
+		"./lib/Tools/print" \
+		"./lib/Tools/scala" \
+		"./lib/Tools/scalac" \
+		"./lib/Tools/tty" \
+		"./lib/Tools/unsymbolize" \
+		"./lib/Tools/usedir" \
+		"./lib/Tools/version" \
+		"./lib/Tools/yxml" \
+		"./lib/browser/build" \
+		"./lib/scripts/feeder" \
+		"./lib/scripts/getsettings" \
+		"./lib/scripts/keywords" \
+		"./lib/scripts/polyml-version" \
+		"./lib/scripts/process" \
+		"./lib/scripts/run-polyml" \
+		"./lib/scripts/run-smlnj" \
+		"./lib/scripts/unsymbolize" \
+		"./lib/scripts/yxml" \
+		"./src/HOL/IMP/export.sh" \
+		"./src/HOL/Library/Sum_of_Squares/neos_csdp_client" \
+		"./src/HOL/Mirabelle/lib/Tools/mirabelle" \
+		"./src/HOL/Mutabelle/lib/Tools/mutabelle" \
+		"./src/HOL/SPARK/Examples/README" \
+		"./src/HOL/TPTP/TPTP_Parser/make_mlyacclib" \
+		"./src/HOL/TPTP/TPTP_Parser/make_tptp_parser" \
+		"./src/HOL/TPTP/lib/Tools/tptp_graph" \
+		"./src/HOL/TPTP/lib/Tools/tptp_isabelle" \
+		"./src/HOL/TPTP/lib/Tools/tptp_isabelle_hot" \
+		"./src/HOL/TPTP/lib/Tools/tptp_nitpick" \
+		"./src/HOL/TPTP/lib/Tools/tptp_refute" \
+		"./src/HOL/TPTP/lib/Tools/tptp_sledgehammer" \
+		"./src/HOL/Tools/ATP/scripts/dummy_atp" \
+		"./src/HOL/Tools/ATP/scripts/remote_atp" \
+		"./src/HOL/Tools/Predicate_Compile/lib/scripts/swipl_version" \
+		"./src/HOL/Tools/SMT/lib/scripts/remote_smt" \
+		"./src/HOL/Tools/Sledgehammer/MaSh/src/compareStats.py" \
+		"./src/HOL/Tools/Sledgehammer/MaSh/src/mash.py" \
+		"./src/Pure/build" \
+		"./src/Pure/build-jars" \
+		"./src/Tools/Code/lib/Tools/codegen" \
+		"./src/Tools/Graphview/lib/Tools/graphview" \
+		"./src/Tools/Metis/fix_metis_license" \
+		"./src/Tools/Metis/make_metis" \
+		"./src/Tools/Metis/scripts/mlpp" \
+		"./src/Tools/WWW_Find/lib/Tools/wwwfind" \
+		"./src/Tools/jEdit/lib/Tools/jedit"
+	do
+		exeinto $(dirname "${TARGETDIR}/${i}")
+		doexe ${i}
+	done
+
+	insinto /etc/isabelle
+	doins -r etc/*
+	dosym /etc/isabelle "${TARGETDIR}/etc"
+
+	dosym "${LIBDIR}/heaps" "${TARGETDIR}/heaps"
+	insinto ${LIBDIR}
+	doins -r heaps
+
+	bin/isabelle install -d ${TARGETDIR} "${ED}usr/bin" \
+		|| die "isabelle install failed"
+	newicon lib/icons/isabelle.xpm "${PN}.xpm"
+	dodoc ANNOUNCE CONTRIBUTORS COPYRIGHT NEWS README
+
+	java-pkg_regjar \
+		"${ED}${TARGETDIR}/contrib/jedit_build-20130104/contrib/Highlight.jar" \
+		"${ED}${TARGETDIR}/contrib/jedit_build-20130104/contrib/ErrorList.jar" \
+		"${ED}${TARGETDIR}/contrib/jedit_build-20130104/contrib/Console.jar" \
+		"${ED}${TARGETDIR}/contrib/jedit_build-20130104/contrib/cobra.jar" \
+		"${ED}${TARGETDIR}/contrib/jedit_build-20130104/contrib/js.jar" \
+		"${ED}${TARGETDIR}/contrib/jedit_build-20130104/contrib/jedit-5.0.0-patched/jedit.jar" \
+		"${ED}${TARGETDIR}/contrib/jedit_build-20130104/contrib/jedit-5.0.0-patched/jars/QuickNotepad.jar" \
+		"${ED}${TARGETDIR}/contrib/jfreechart-1.0.14/jfreechart-1.0.14-demo.jar" \
+		"${ED}${TARGETDIR}/lib/classes/ext/Graphview.jar" \
+		"${ED}${TARGETDIR}/lib/classes/ext/Pure.jar" \
+		"${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/Console.jar" \
+		"${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/ErrorList.jar" \
+		"${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/Highlight.jar" \
+		"${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/Isabelle-jEdit.jar" \
+		"${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/QuickNotepad.jar" \
+		"${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/SideKick.jar" \
+		"${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/cobra.jar" \
+		"${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/js.jar" \
+		"${ED}${TARGETDIR}/src/Tools/jEdit/dist/jedit.jar"
+}
+
+pkg_postinst() {
+	# If any of the directories in /etc/isabelle/components do not exist, then
+	# even isabelle getenv ISABELLE_HOME fails.  Hence it is necessary to
+	# to delete any non-existing directories.  If an old Isabelle version was
+	# installed with component ebuilds like sci-mathematics/e, then the
+	# Isabelle version is upgraded, then the contrib directories will not
+	# exist initially, it is necessary to delete them from /etc/isabelle/components.
+	# Then these components are rebuilt (creating these directories) using the
+	# EAPI=5 subslot depends.
+	for i in $(egrep '^[^#].*$' "${ROOT}etc/isabelle/components")
+	do
+		if [ ! -d /usr/share/${MY_P}/${i} ]; then
+			sed -e "\@${i}@d" -i "${ROOT}etc/isabelle/components"
+		fi
+	done
+	if use ledit && use readline; then
+		elog "Both readline and ledit use flags specified.  The default setting"
+		elog "if both are installed is to use readline (rlwrap), this can be"
+		elog "modfied by editing the ISABELLE_LINE_EDITOR setting in"
+		elog "${ROOT}/etc/isabelle/settings"
+	fi
+	elog "Please ensure you have a pdf viewer installed, for example:"
+	elog "As root: emerge app-text/zathura-pdf-poppler"
+	elog "Please configure your preferred pdf viewer, something like:"
+	elog "As normal user: xdg-mime default zathura.desktop application/pdf"
+	elog "Or alternatively by editing the PDF_VIEWER variable in the system"
+	elog "settings file ${ROOT}etc/isabelle/settings and/or the user"
+	elog "settings file \$HOME/.isabelle/${MY_P}/etc/settings"
+	elog "To improve sledgehammer performance, consider installing:"
+	elog "USE=isabelle emerge sci-mathematics/e sci-mathematics/spass"
+	elog "For nitpick it is necessary to install:"
+	elog "emerge sci-mathematics/kodkodi"
+}