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).

(Portage version: 2.1.10.63/cvs/Linux x86_64)

9 files changed, 687 insertions, 1 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/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>