Bump to 2011.1-r1 and 2012. Add jedit use flag to build Isabelle/jEdit Prover IDE (PIDE) (2012 only, requires dev-lang/scala), ledit and readline use flags for the preferred tty line editor. Add dev-perl/libwww-perl dep. Add doc-src directory with use=doc (2012) as doc-src stuff is required when building doc some isabelle add on packages (sci-mathematics/haskabelle).

Package-Manager: portage-2.1.10.63/cvs/Linux x86_64

10 files changed, 702 insertions, 6 deletions

diff --git a/sci-mathematics/isabelle/ChangeLog b/sci-mathematics/isabelle/ChangeLog
index c2ba2bd7f436..5f501379ce89 100644
--- a/sci-mathematics/isabelle/ChangeLog
+++ b/sci-mathematics/isabelle/ChangeLog
@@ -1,6 +1,21 @@
 # ChangeLog for sci-mathematics/isabelle
 # Copyright 1999-2012 Gentoo Foundation; Distributed under the GPL v2
-# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/isabelle/ChangeLog,v 1.3 2012/01/30 06:54:53 gienah Exp $
+# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/isabelle/ChangeLog,v 1.4 2012/05/30 00:45:06 gienah Exp $
+
+*isabelle-2012 (30 May 2012)
+*isabelle-2011.1-r1 (30 May 2012)
+
+  30 May 2012; Mark Wright <gienah@gentoo.org> +isabelle-2011.1-r1.ebuild,
+  +files/isabelle-2011.1-gentoo-settings.patch,
+  +files/isabelle-2011.1-reverse-line-editor-order.patch,
+  +isabelle-2012.ebuild, +files/isabelle-2012-gentoo-settings.patch,
+  +files/isabelle-2012-graphbrowser.patch,
+  +files/isabelle-2012-reverse-line-editor-order.patch, metadata.xml:
+  Bump to 2011.1-r1 and 2012. Add jedit use flag to build Isabelle/jEdit Prover
+  IDE (PIDE) (2012 only, requires dev-lang/scala), ledit and readline use flags
+  for the preferred tty line editor. Add dev-perl/libwww-perl dep. Add doc-src
+  directory with use=doc (2012) as doc-src stuff is required when building doc
+  some isabelle add on packages (sci-mathematics/haskabelle).
 
   30 Jan 2012; Mark Wright <gienah@gentoo.org> isabelle-2011.1.ebuild,
   metadata.xml:
diff --git a/sci-mathematics/isabelle/Manifest b/sci-mathematics/isabelle/Manifest
index 02ab9c7d0232..a23c7de6dead 100644
--- a/sci-mathematics/isabelle/Manifest
+++ b/sci-mathematics/isabelle/Manifest
@@ -1,16 +1,26 @@
 -----BEGIN PGP SIGNED MESSAGE-----
 Hash: SHA256
 
+AUX isabelle-2011.1-gentoo-settings.patch 1265 RMD160 9060454ab5480056b931b7a663137c80efa73b42 SHA1 e447977ddfbf08de46695f7b63e0ce2af3b55ac5 SHA256 08f6dae3f3157331ac83a3204f95e75838725175994c54f25b5f71715836556a
 AUX isabelle-2011.1-graphbrowser.patch 358 RMD160 debe029504aad72c611f783569ca6e5e07d6fcfa SHA1 5067aa4f60a9185d6b7ca2e4d9511dd93ed6f239 SHA256 3c4a1567e06ea062f3064a7fb4555a645591732dc2d77daf7b4c49de6f640115
 AUX isabelle-2011.1-proofgeneral-gentoo-path.patch 1265 RMD160 9060454ab5480056b931b7a663137c80efa73b42 SHA1 e447977ddfbf08de46695f7b63e0ce2af3b55ac5 SHA256 08f6dae3f3157331ac83a3204f95e75838725175994c54f25b5f71715836556a
+AUX isabelle-2011.1-reverse-line-editor-order.patch 427 RMD160 b3c672e939541e3eeb2f4a866628c668cd5d2898 SHA1 9095831f761de457915a10a5391a260de4b8b910 SHA256 1a664c94d400d88dfa5af9af3bdb4c90bacd12792286b3c4933f62ca15e5b9a0
+AUX isabelle-2012-gentoo-settings.patch 2107 RMD160 4ebd777b8c498a833d0264ddf67f367003a424f2 SHA1 b073aae7982a29bfc200c985e53051b882f3aa7d SHA256 5076d6665b367a9b08a2e56ba901028e90910a444c2c02322ebf8d9d9ac328b1
+AUX isabelle-2012-graphbrowser.patch 354 RMD160 68eaee7f3e8c8b92f608cf5936ea8a4315634b41 SHA1 508be51f17ad6bf08d5df71535298f42177a736a SHA256 0b6d3a3736ec89ad870ef24bb2ba3c2006a907e1a29a113e3f63a5ad609ec4b7
+AUX isabelle-2012-reverse-line-editor-order.patch 423 RMD160 6a51017a64f70fde99decfb2e0b09e281836ec6b SHA1 ff5945dd644dba3b0fd0fcd49ec793e9bf10c2ae SHA256 51a172b46baaaa269488801bad3d46ba4ccd0e3df35b2c15dc9b75592ceb843e
 DIST Isabelle2011-1.tar.gz 42239059 RMD160 70dadeaf38ae71ff9871f8c5b9ba823c4d5cbcc7 SHA1 2f514bc2cff7e7f7c75a3cb15c71ea71009f8df7 SHA256 48d77fe31a16b44f6015aa7953a60bdad8fcec9e60847630dc7b98c053edfc08
+DIST Isabelle2012-doc-src.tar.gz 2688496 RMD160 cbef295dc2f6b27ab32815b9395dc38f0f344ea8 SHA1 2ed623a40488b7c200282457c240af575fe4b3e6 SHA256 e18965fe0f7f89b286d4707e38201f1edbea81f6b26aed59d63a633c03fec097
+DIST Isabelle2012.tar.gz 49529865 RMD160 62de99689ba65e2d4ff02d9590397db3d3115cf0 SHA1 9ec664d48bb15b679c7316820aa03ba37d6fc56b SHA256 b86f957dee221041f92c9d4ced4758d45b4950339743d0d58b1ea6061e2b53f0
+DIST jedit_build-20120414.tar.gz 7509120 RMD160 f3977207db8df6ccaf85015640a938cc3a475c4c SHA1 6425f622625024c1de27f3730d6811f6370a19cd SHA256 3c5840fd01b87013b05a92742d41f66f655df6fe9edef1525c6722f92d8f3e41
+EBUILD isabelle-2011.1-r1.ebuild 7158 RMD160 a6638676fb40ef87eb2ed3076b8618a451c641d7 SHA1 dfcdf9aa011a72236c5718bc16b08c31d45498fa SHA256 4a751a8893be2d92e4e1d709209ee94f68f3555e73c045136fb41ea83b918a1c
 EBUILD isabelle-2011.1.ebuild 4036 RMD160 363ef11acf50946dcde1151643e053d7c1064339 SHA1 cc9e14c8b1893c03d2efcdfd0262710b23d725e3 SHA256 6063b32c39e50c42e81051197ce46a735bb16448c13b5ff1f8af5018f07b3020
-MISC ChangeLog 869 RMD160 b9786ff70293c601da7fb575f5779fce748625d1 SHA1 cb2d331ef6961136bf39779cb3161e97789d11c9 SHA256 3e6dfcd4763b0de4d35b8789fadd7384ab1b9f90bd71fa00e38f9f3f13880fef
-MISC metadata.xml 1928 RMD160 437eb8bfd6958ef1da0444d1fd649b185ca80348 SHA1 09fc04f42bd66e10c610bf27d0596cfc329e5476 SHA256 358d11a2caf5a5608686637b16f7c842fbe043504f39984835e1f8b9751f8ef7
+EBUILD isabelle-2012.ebuild 9776 RMD160 9720486c161c7da9f91e35a8da831e6261679274 SHA1 1ada1c0433db06f3922c2a5f48dbc886f8dd9dd4 SHA256 a830baad156e332e30e44a4b64a77d74c78b7ec6f11aa21ebba30e52bd245d96
+MISC ChangeLog 1677 RMD160 f7e6e9579f92c0ddb4fc3073a82b76229f9d75c6 SHA1 7e1ad7c49bc7d49fe7609ebed7b0e35f5eef319c SHA256 cea75b42cd88b33a1ac5664a8bdbe0cd213c1d3f14fea91ea5a954f2148acd5d
+MISC metadata.xml 2157 RMD160 ee8247053938f0b3686a6e0ea8dbfe0cf925a700 SHA1 459ec3cc74b389f410d26c2da55bb89a5d842a11 SHA256 bdcce608d1d69f75e4aa0c809f85885dd025cd9ed2c1a12552a446033c4a7fa6
 -----BEGIN PGP SIGNATURE-----
 Version: GnuPG v2.0.17 (GNU/Linux)
 
-iF4EAREIAAYFAk8mPswACgkQoBEVQmGOlx/f7QEAq0804KhSJXJSSU1Wa1nD01dN
-LF85jMEvW+24Z9ZckgoBAMs0deFFYiBpJ8GeCXlWU1phC1BdoZOnID+lzSUqa7cc
-=1qfF
+iF4EAREIAAYFAk/FbaIACgkQoBEVQmGOlx/UQAEAwuUYY2arR5bF3refK8UCYYdr
+QiY7mn286hs+ktiE5BUBAJ7Clx9wfej5m8lgWVNdobPwTmg9pJIc4VBKXuTjqHSF
+=BVGh
 -----END PGP SIGNATURE-----
diff --git a/sci-mathematics/isabelle/files/isabelle-2011.1-gentoo-settings.patch b/sci-mathematics/isabelle/files/isabelle-2011.1-gentoo-settings.patch
new file mode 100644
index 000000000000..67e3476f2170
--- /dev/null
+++ b/sci-mathematics/isabelle/files/isabelle-2011.1-gentoo-settings.patch
@@ -0,0 +1,39 @@
+--- Isabelle2011-1-orig/etc/settings	2011-10-10 01:47:58.000000000 +1100
++++ Isabelle2011-1/etc/settings	2012-01-01 16:33:27.922565527 +1100
+@@ -24,9 +24,16 @@
+   "/usr/share/polyml/$ML_PLATFORM" \
+   "/opt/polyml/$ML_PLATFORM" \
+   "")"
+-ML_SYSTEM=$("$ISABELLE_HOME/lib/scripts/polyml-version")
+-ML_OPTIONS="-H 200"
+-ML_SOURCES="$ML_HOME/../src"
++# ML_SYSTEM=$("$ISABELLE_HOME/lib/scripts/polyml-version")
++# ML_OPTIONS="-H 200"
++# ML_SOURCES="$ML_HOME/../src"
++
++# Poly/ML 5.4.0 (64 bit)
++ML_PLATFORM=x86_64-linux
++ML_HOME=/usr/bin
++ML_SYSTEM=polyml-5.4.0
++ML_OPTIONS="-H 1000"
++#ML_SOURCES="$ML_HOME/../src"
+ 
+ # Poly/ML 32 bit (manual settings)
+ #ML_SYSTEM=polyml-5.4.0
+@@ -106,7 +113,7 @@
+ ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
+ 
+ # Heap input locations. ML system identifier is included in lookup.
+-ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
++ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:/usr/lib64/Isabelle2011-1/heaps"
+ 
+ # Heap output location. ML system identifier is appended automatically later on.
+ ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
+@@ -170,6 +177,7 @@
+   "/usr/local/ProofGeneral" \
+   "/usr/share/ProofGeneral" \
+   "/opt/ProofGeneral" \
++  "/usr/share/emacs/site-lisp/ProofGeneral" \
+   "")"
+ 
+ PROOFGENERAL_OPTIONS=""
diff --git a/sci-mathematics/isabelle/files/isabelle-2011.1-reverse-line-editor-order.patch b/sci-mathematics/isabelle/files/isabelle-2011.1-reverse-line-editor-order.patch
new file mode 100644
index 000000000000..b2f2c35ee087
--- /dev/null
+++ b/sci-mathematics/isabelle/files/isabelle-2011.1-reverse-line-editor-order.patch
@@ -0,0 +1,12 @@
+--- Isabelle2011-1-orig/etc/settings	2011-10-10 01:47:58.000000000 +1100
++++ Isabelle2011-1/etc/settings	2012-05-27 23:28:37.283028668 +1000
+@@ -66,8 +66,8 @@
+ ###
+ 
+ ISABELLE_LINE_EDITOR=""
+-[ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p rlwrap)"
+ [ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p ledit)"
++[ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p rlwrap)"
+ 
+ 
+ ###
diff --git a/sci-mathematics/isabelle/files/isabelle-2012-gentoo-settings.patch b/sci-mathematics/isabelle/files/isabelle-2012-gentoo-settings.patch
new file mode 100644
index 000000000000..8994491445d5
--- /dev/null
+++ b/sci-mathematics/isabelle/files/isabelle-2012-gentoo-settings.patch
@@ -0,0 +1,62 @@
+--- Isabelle2012-orig/etc/settings	2012-05-23 03:07:38.000000000 +1000
++++ Isabelle2012/etc/settings	2012-05-27 18:07:26.502878614 +1000
+@@ -16,17 +16,24 @@
+ # Only one of the sections below should be activated.
+ 
+ # Poly/ML default (automated settings)
+-ML_PLATFORM="$ISABELLE_PLATFORM"
+-ML_HOME="$(choosefrom \
+-  "$ISABELLE_HOME/contrib/polyml/$ML_PLATFORM" \
+-  "$ISABELLE_HOME/../polyml/$ML_PLATFORM" \
+-  "/usr/local/polyml/$ML_PLATFORM" \
+-  "/usr/share/polyml/$ML_PLATFORM" \
+-  "/opt/polyml/$ML_PLATFORM" \
+-  "")"
+-ML_SYSTEM=$("$ISABELLE_HOME/lib/scripts/polyml-version")
+-ML_OPTIONS="-H 200"
+-ML_SOURCES="$ML_HOME/../src"
++# ML_PLATFORM="$ISABELLE_PLATFORM"
++# ML_HOME="$(choosefrom \
++#   "$ISABELLE_HOME/contrib/polyml/$ML_PLATFORM" \
++#   "$ISABELLE_HOME/../polyml/$ML_PLATFORM" \
++#   "/usr/local/polyml/$ML_PLATFORM" \
++#   "/usr/share/polyml/$ML_PLATFORM" \
++#   "/opt/polyml/$ML_PLATFORM" \
++#   "")"
++# ML_SYSTEM=$("$ISABELLE_HOME/lib/scripts/polyml-version")
++# ML_OPTIONS="-H 200"
++# ML_SOURCES="$ML_HOME/../src"
++
++# Poly/ML Gentoo (x86_64)
++ML_PLATFORM=x86_64-linux
++ML_HOME="/usr/bin"
++ML_SYSTEM=polyml-5.4.0
++ML_OPTIONS="-H 1000"
++ML_SOURCES="/usr/src/debug/dev-lang/polyml-5.4.0"
+ 
+ # Poly/ML 32 bit (manual settings)
+ #ML_SYSTEM=polyml-5.4.1
+@@ -102,7 +109,7 @@
+ ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
+ 
+ # Heap input locations. ML system identifier is included in lookup.
+-ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
++ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:/usr/lib64/Isabelle2012/heaps"
+ 
+ # Heap output location. ML system identifier is appended automatically later on.
+ ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
+@@ -161,13 +168,7 @@
+ ###
+ 
+ # Proof General home, look in a variety of places
+-PROOFGENERAL_HOME="$(choosefrom \
+-  "$ISABELLE_HOME/contrib/ProofGeneral" \
+-  "$ISABELLE_HOME/../ProofGeneral" \
+-  "/usr/local/ProofGeneral" \
+-  "/usr/share/ProofGeneral" \
+-  "/opt/ProofGeneral" \
+-  "")"
++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/files/isabelle-2012-graphbrowser.patch b/sci-mathematics/isabelle/files/isabelle-2012-graphbrowser.patch
new file mode 100644
index 000000000000..3e63f1c62237
--- /dev/null
+++ b/sci-mathematics/isabelle/files/isabelle-2012-graphbrowser.patch
@@ -0,0 +1,11 @@
+--- Isabelle2012-orig/lib/browser/build	2012-05-20 19:34:33.000000000 +1000
++++ Isabelle2012/lib/browser/build	2012-05-26 22:18:41.952750622 +1000
+@@ -6,6 +6,8 @@
+ #
+ # Requires proper Isabelle settings environment.
+ 
++ISABELLE_HOME="$(cd "$(dirname "${0}")/../.."; pwd -P)"
++source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
+ 
+ ## diagnostics
+ 
diff --git a/sci-mathematics/isabelle/files/isabelle-2012-reverse-line-editor-order.patch b/sci-mathematics/isabelle/files/isabelle-2012-reverse-line-editor-order.patch
new file mode 100644
index 000000000000..233ea5b50fad
--- /dev/null
+++ b/sci-mathematics/isabelle/files/isabelle-2012-reverse-line-editor-order.patch
@@ -0,0 +1,12 @@
+--- Isabelle2012-orig/etc/settings	2012-05-23 03:07:38.000000000 +1000
++++ Isabelle2012/etc/settings	2012-05-27 12:43:36.209715015 +1000
+@@ -62,8 +62,8 @@
+ ###
+ 
+ ISABELLE_LINE_EDITOR=""
+-[ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p rlwrap)"
+ [ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p ledit)"
++[ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p rlwrap)"
+ 
+ 
+ ###
diff --git a/sci-mathematics/isabelle/isabelle-2011.1-r1.ebuild b/sci-mathematics/isabelle/isabelle-2011.1-r1.ebuild
new file mode 100644
index 000000000000..4719507e7d75
--- /dev/null
+++ b/sci-mathematics/isabelle/isabelle-2011.1-r1.ebuild
@@ -0,0 +1,233 @@
+# Copyright 1999-2012 Gentoo Foundation
+# Distributed under the terms of the GNU General Public License v2
+# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/isabelle/isabelle-2011.1-r1.ebuild,v 1.1 2012/05/30 00:45:06 gienah Exp $
+
+EAPI="4"
+
+inherit eutils java-pkg-2 multilib versionator
+
+MY_PN="Isabelle"
+MY_PV=$(replace_all_version_separators '-')
+MY_P="${MY_PN}${MY_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"
+
+LICENSE="BSD"
+SLOT="0"
+KEYWORDS="~x86 ~amd64"
+ALL_LOGICS="Pure FOL +HOL ZF CCL CTT Cube FOLP LCF Sequents"
+IUSE="${ALL_LOGICS} doc graphbrowsing ledit readline +proofgeneral test"
+
+#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-lang/polyml-5.4.1[-portable]
+		>=dev-lang/perl-5.8.8-r2"
+
+RDEPEND="dev-perl/libwww-perl
+	doc? (
+		virtual/latex-base
+		dev-tex/rail
+	)
+	proofgeneral? (
+		app-emacs/proofgeneral
+	)
+	ledit? (
+		app-misc/ledit
+	)
+	readline? (
+		app-misc/rlwrap
+	)
+	${DEPEND}"
+
+S="${WORKDIR}"/Isabelle${MY_PV}
+TARGETDIR="/usr/share/Isabelle"${MY_PV}
+LIBDIR="/usr/"$(get_libdir)"/Isabelle"${MY_PV}
+
+pkg_setup() {
+	java-pkg-2_pkg_setup
+	if ! use proofgeneral
+	then
+		ewarn "You have deselected the Proof General interface."
+		ewarn "Only a text terminal will be installed."
+		ewarn "Emerge Isabelle with the proofgeneral USE flag enabled"
+		ewarn "to get the common interface, that most people want."
+	fi
+}
+
+src_prepare() {
+	java-pkg-2_src_prepare
+	epatch "${FILESDIR}/${PN}-2011.1-gentoo-settings.patch"
+	polymlver=$(poly -v | cut -d' ' -f2)
+	polymlarch=$(poly -v | cut -d' ' -f9 | cut -d'-' -f1)
+	sed -e "s@5.4.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}-2011.1-graphbrowser.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"
+	EOF
+	if use ledit && !use readline; then
+		epatch "${FILESDIR}/${PN}-2011.1-reverse-line-editor-order.patch"
+	fi
+}
+
+src_compile() {
+	LOGICS=""
+	for l in "${ALL_LOGICS}"; do
+		if has "${l/+/}"; then
+			LOGICS="${LOGICS} ${l/+/}"
+		fi
+	done
+	einfo "Building Isabelle logics ${LOGICS}. This may take some time."
+	./build -b -i "${LOGICS}" || die "building logics failed"
+	./bin/isabelle makeall || die "isabelle makeall failed"
+	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
+}
+
+src_test() {
+	einfo "Running tests. A test run can take up to several hours!"
+	./build -b -t || die "tests failed"
+}
+
+src_install() {
+	exeinto ${TARGETDIR}/bin
+	doexe bin/isabelle-process bin/isabelle
+
+	insinto ${TARGETDIR}
+	doins -r src
+	doins -r lib
+
+	for i in "./build" \
+		"src/Pure/mk" \
+		"src/Pure/build-jars" \
+		"src/Tools/jEdit/dist/build-support/ci/copy_properties.groovy" \
+		"src/Tools/jEdit/dist/build-support/ci/ci_release.groovy" \
+		"src/Tools/jEdit/lib/Tools/jedit" \
+		"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/Code/lib/Tools/codegen" \
+		"src/HOL/Mirabelle/lib/Tools/mirabelle" \
+		"src/HOL/Tools/Predicate_Compile/lib/scripts/swipl_version" \
+		"src/HOL/Tools/SMT/lib/scripts/remote_smt" \
+		"src/HOL/Tools/ATP/scripts/remote_atp" \
+		"src/HOL/Tools/ATP/scripts/spass" \
+		"src/HOL/Tools/Nitpick/lib/Tools/nitrox" \
+		"src/HOL/Mutabelle/lib/Tools/mutabelle" \
+		"src/HOL/Library/Sum_of_Squares/neos_csdp_client" \
+		"lib/browser/build" \
+		"lib/Tools/tty" \
+		"lib/Tools/mkproject" \
+		"lib/Tools/keywords" \
+		"lib/Tools/browser" \
+		"lib/Tools/install" \
+		"lib/Tools/mkdir" \
+		"lib/Tools/unsymbolize" \
+		"lib/Tools/getenv" \
+		"lib/Tools/java" \
+		"lib/Tools/make" \
+		"lib/Tools/emacs" \
+		"lib/Tools/scala" \
+		"lib/Tools/print" \
+		"lib/Tools/latex" \
+		"lib/Tools/findlogics" \
+		"lib/Tools/doc" \
+		"lib/Tools/logo" \
+		"lib/Tools/usedir" \
+		"lib/Tools/yxml" \
+		"lib/Tools/version" \
+		"lib/Tools/makeall" \
+		"lib/Tools/scalac" \
+		"lib/Tools/document" \
+		"lib/Tools/env" \
+		"lib/Tools/display" \
+		"lib/Tools/dimacs2hol" \
+		"lib/scripts/keywords" \
+		"lib/scripts/unsymbolize" \
+		"lib/scripts/run-polyml" \
+		"lib/scripts/run-smlnj" \
+		"lib/scripts/feeder" \
+		"lib/scripts/java_ext_dirs" \
+		"lib/scripts/yxml" \
+		"lib/scripts/raw_dump" \
+		"lib/scripts/polyml-version" \
+		"lib/scripts/process"
+	do
+		exeinto $(dirname "${TARGETDIR}/${i}")
+		doexe ${i}
+	done
+
+	docompress -x /usr/share/doc/${PF}
+	dodoc -r doc
+
+	dodir /etc/isabelle
+	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} -p "${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}/lib/browser/GraphBrowser.jar" \
+		"${ED}${TARGETDIR}/lib/classes/ext/Pure.jar" \
+		"${ED}${TARGETDIR}/lib/classes/ext/scala-library.jar" \
+		"${ED}${TARGETDIR}/lib/classes/ext/scala-swing.jar" \
+		"${ED}${TARGETDIR}/lib/classes/java_ext_dirs.jar"
+}
+
+pkg_postinst() {
+	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 "You will need to re-emerge Isabelle after emerging polyml."
+	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"
+}
diff --git a/sci-mathematics/isabelle/isabelle-2012.ebuild b/sci-mathematics/isabelle/isabelle-2012.ebuild
new file mode 100644
index 000000000000..3d66f3f4ece9
--- /dev/null
+++ b/sci-mathematics/isabelle/isabelle-2012.ebuild
@@ -0,0 +1,298 @@
+# Copyright 1999-2012 Gentoo Foundation
+# Distributed under the terms of the GNU General Public License v2
+# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/isabelle/isabelle-2012.ebuild,v 1.1 2012/05/30 00:45:06 gienah Exp $
+
+EAPI="4"
+
+inherit eutils java-pkg-2 multilib versionator
+
+MY_PN="Isabelle"
+MY_PV=$(replace_all_version_separators '-')
+MY_P="${MY_PN}${MY_PV}"
+
+JEDIT_PV="20120414"
+JEDIT_PN="jedit_build"
+JEDIT_P="${JEDIT_PN}-${JEDIT_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
+		doc? ( http://dev.gentoo.org/~gienah/snapshots/${MY_P}-doc-src.tar.gz )
+		pide? ( http://www4.in.tum.de/~wenzelm/test/${JEDIT_P}.tar.gz )"
+
+LICENSE="BSD"
+SLOT="0"
+KEYWORDS="~x86 ~amd64"
+ALL_LOGICS="Pure FOL +HOL ZF CCL CTT Cube FOLP LCF Sequents"
+IUSE="${ALL_LOGICS} doc graphbrowsing ledit readline pide +proofgeneral test"
+
+#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-lang/polyml-5.4.1[-portable]
+		>=dev-lang/perl-5.8.8-r2"
+
+RDEPEND="dev-perl/libwww-perl
+	doc? (
+		virtual/latex-base
+		dev-tex/rail
+	)
+	proofgeneral? (
+		app-emacs/proofgeneral
+	)
+	pide? (
+		>=dev-lang/scala-2.8.2
+	)
+	ledit? (
+		app-misc/ledit
+	)
+	readline? (
+		app-misc/rlwrap
+	)
+	${DEPEND}"
+
+S="${WORKDIR}"/Isabelle${MY_PV}
+JEDIT_S="${WORKDIR}/${JEDIT_P}"
+TARGETDIR="/usr/share/Isabelle"${MY_PV}
+LIBDIR="/usr/"$(get_libdir)"/Isabelle"${MY_PV}
+
+pkg_setup() {
+	java-pkg-2_pkg_setup
+	if ! use proofgeneral
+	then
+		ewarn "You have deselected the Proof General interface."
+		ewarn "Only a text terminal will be installed."
+		ewarn "Emerge Isabelle with the proofgeneral USE flag enabled"
+		ewarn "to get the common interface, that most people want."
+	fi
+}
+
+src_prepare() {
+	java-pkg-2_src_prepare
+	epatch "${FILESDIR}/${PN}-2012-gentoo-settings.patch"
+	polymlver=$(poly -v | cut -d' ' -f2)
+	polymlarch=$(poly -v | cut -d' ' -f9 | cut -d'-' -f1)
+	sed -e "s@5.4.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"
+	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"
+	EOF
+	if use pide; then
+		cat <<- EOF >> "${S}/etc/settings"
+			ISABELLE_JEDIT_BUILD_HOME="\$ISABELLE_HOME/${JEDIT_P}"
+			init_component ${JEDIT_S}
+		EOF
+	fi
+	if use ledit && !use readline; then
+		epatch "${FILESDIR}/${PN}-2012-reverse-line-editor-order.patch"
+	fi
+}
+
+src_compile() {
+	LOGICS=""
+	for l in "${ALL_LOGICS}"; do
+		if has "${l/+/}"; then
+			LOGICS="${LOGICS} ${l/+/}"
+		fi
+	done
+	einfo "Building Isabelle logics ${LOGICS}. This may take some time."
+	./build -b -i "${LOGICS}" || die "building logics failed"
+	./bin/isabelle makeall || die "isabelle makeall failed"
+	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
+	if use pide; then
+		pushd "${S}/src/Tools/jEdit" \
+			|| die "Could not change directory to src/Tools/jEdit"
+		"${S}"/bin/isabelle jedit -b -f \
+			|| die "pide build failed"
+		popd
+		# The jedit_build stuff is only required to build
+		# Isabelle/jEdit Prover IDE (PIDE).  These 2 lines need to be deleted
+		# from etc/settings as the jedit_build source code is not installed
+		sed -e '/ISABELLE_JEDIT_BUILD_HOME/d' \
+			-e '/init_component/d' \
+			-i "${S}/etc/settings" \
+			|| die "Could not delete jedit_build lines from etc/settings"
+	fi
+}
+
+src_test() {
+	einfo "Running tests. A test run can take up to several hours!"
+	./build -b -t || die "tests failed"
+}
+
+src_install() {
+	exeinto ${TARGETDIR}/bin
+	doexe bin/isabelle-process bin/isabelle
+
+	insinto ${TARGETDIR}
+	doins -r src
+	doins -r lib
+
+	if use doc; then
+		# The build of sci-mathematics/haskabelle with use doc requires
+		# sci-mathematics/isabelle[doc?]. The haskabelle doc build requires
+		# the doc-src directory stuff in the isabelle package.  Which is not
+		# provided in the Isabelle 2012 src tarball.  So extract it from a
+		# snapshot of the isabelle repo taken soon after the Isabelle 2012
+		# release.
+		doins -r doc-src
+		for i in "./doc-src/IsarRef/showsymbols" \
+			"./doc-src/TutorialI/Overview/LNCS/makeDemo" \
+			"./doc-src/TutorialI/isa-index" \
+			"./doc-src/sedindex"
+		do
+			exeinto $(dirname "${TARGETDIR}/${i}")
+			doexe ${i}
+		done
+	fi
+
+	for i in "./build" \
+		"./src/Pure/mk" \
+		"./src/Pure/build-jars" \
+		"./src/Tools/JVM/build" \
+		"./src/Tools/JVM/java_ext_dirs" \
+		"./src/Tools/jEdit/lib/Tools/jedit" \
+		"./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/Code/lib/Tools/codegen" \
+		"./src/HOL/Mirabelle/lib/Tools/mirabelle" \
+		"./src/HOL/Tools/Predicate_Compile/lib/scripts/swipl_version" \
+		"./src/HOL/Tools/SMT/lib/scripts/remote_smt" \
+		"./src/HOL/Tools/ATP/scripts/remote_atp" \
+		"./src/HOL/Tools/ATP/scripts/spass" \
+		"./src/HOL/Mutabelle/lib/Tools/mutabelle" \
+		"./src/HOL/TPTP/TPTP_Parser/make_mlyacclib" \
+		"./src/HOL/TPTP/TPTP_Parser/make_tptp_parser" \
+		"./src/HOL/TPTP/lib/Tools/tptp_isabelle_demo" \
+		"./src/HOL/TPTP/lib/Tools/tptp_graph" \
+		"./src/HOL/TPTP/lib/Tools/tptp_isabelle_comp" \
+		"./src/HOL/TPTP/lib/Tools/tptp_refute" \
+		"./src/HOL/TPTP/lib/Tools/tptp_translate" \
+		"./src/HOL/TPTP/lib/Tools/tptp_sledgehammer" \
+		"./src/HOL/TPTP/lib/Tools/tptp_nitpick" \
+		"./src/HOL/Library/Sum_of_Squares/neos_csdp_client" \
+		"./src/HOL/IMP/export.sh" \
+		"./lib/browser/build" \
+		"./lib/Tools/tty" \
+		"./lib/Tools/mkproject" \
+		"./lib/Tools/keywords" \
+		"./lib/Tools/browser" \
+		"./lib/Tools/install" \
+		"./lib/Tools/mkdir" \
+		"./lib/Tools/unsymbolize" \
+		"./lib/Tools/getenv" \
+		"./lib/Tools/java" \
+		"./lib/Tools/make" \
+		"./lib/Tools/emacs" \
+		"./lib/Tools/scala" \
+		"./lib/Tools/print" \
+		"./lib/Tools/latex" \
+		"./lib/Tools/findlogics" \
+		"./lib/Tools/doc" \
+		"./lib/Tools/logo" \
+		"./lib/Tools/usedir" \
+		"./lib/Tools/yxml" \
+		"./lib/Tools/version" \
+		"./lib/Tools/makeall" \
+		"./lib/Tools/scalac" \
+		"./lib/Tools/document" \
+		"./lib/Tools/env" \
+		"./lib/Tools/display" \
+		"./lib/Tools/dimacs2hol" \
+		"./lib/scripts/keywords" \
+		"./lib/scripts/unsymbolize" \
+		"./lib/scripts/run-polyml" \
+		"./lib/scripts/run-smlnj" \
+		"./lib/scripts/feeder" \
+		"./lib/scripts/yxml" \
+		"./lib/scripts/polyml-version" \
+		"./lib/scripts/process"
+	do
+		exeinto $(dirname "${TARGETDIR}/${i}")
+		doexe ${i}
+	done
+
+	docompress -x /usr/share/doc/${PF}
+	dodoc -r doc
+
+	dodir /etc/isabelle
+	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} -p "${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}/src/Tools/JVM/java_ext_dirs.jar" \
+		"${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/QuickNotepad.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/Hyperlinks.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/jars/scala-compiler.jar" \
+		"${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/Isabelle-jEdit.jar" \
+		"${ED}${TARGETDIR}/src/Tools/jEdit/dist/jedit.jar" \
+		"${ED}${TARGETDIR}/lib/classes/ext/scala-swing.jar" \
+		"${ED}${TARGETDIR}/lib/classes/ext/scala-library.jar" \
+		"${ED}${TARGETDIR}/lib/classes/ext/Pure.jar" \
+		"${ED}${TARGETDIR}/lib/browser/GraphBrowser.jar"
+}
+
+pkg_postinst() {
+	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 "You will need to re-emerge Isabelle after emerging polyml."
+	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"
+}
diff --git a/sci-mathematics/isabelle/metadata.xml b/sci-mathematics/isabelle/metadata.xml
index 099959fac571..cb9e26433e7f 100644
--- a/sci-mathematics/isabelle/metadata.xml
+++ b/sci-mathematics/isabelle/metadata.xml
@@ -33,7 +33,11 @@ properties of computer languages and protocols.
   including HTML documents that show a theory's definition, the
   theorems proved in its ML file and the relationship with its
   ancestors and descendants.</flag>
+  <flag name='ledit'>Use ledit for the isabelle tty line editor</flag> 
+  <flag name='readline'>Use readline (rlwrap) for the isabelle tty line
+  editor</flag> 
   <flag name='proofgeneral'>Add support for the
   <pkg>app-emacs/proofgeneral</pkg> proof assistant front end.</flag>
+  <flag name='pide'>Build Isabelle/jEdit Prover IDE (PIDE).</flag> 
 </use>
 </pkgmetadata>