# Copyright 1999-2009 Gentoo Foundation
# Distributed under the terms of the GNU General Public License v2
# $Header: $

EAPI="2"

inherit eutils multilib

DESCRIPTION="Isabelle is a generic proof assistant"
HOMEPAGE="http://isabelle.in.tum.de/ http://www.cl.cam.ac.uk/research/hvg/Isabelle/"
SRC_URI="http://isabelle.in.tum.de/dist/Isabelle${PV}.tar.gz"

LICENSE="BSD"
SLOT="0"
KEYWORDS="~x86 ~amd64"
IUSE="doc graphbrowsing +proofgeneral"


#upstream says
#bash 2.x/3.x, Poly/ML 5.x, Perl 5.x,
#for Proof General GNU Emacs 21/22, xemacs 21.4.x, NOT xemacs 21.5 beta
#for document preparation: complete LaTeX
DEPEND=">=app-shells/bash-3.0
	graphbrowsing? (
		virtual/jdk
	)"

#proofgeneral uses eclass elisp that depends on virtual/emacs-21
RDEPEND=">=dev-lang/polyml-5.2.1
	>=dev-lang/perl-5.8.8-r2
	doc? (
		virtual/latex-base
	)
	proofgeneral? (
		app-emacs/proofgeneral
	)
	${DEPEND}"

S="${WORKDIR}"/Isabelle${PV}
TARGETDIR="/usr/share/Isabelle"${PV}
LIBDIR="/usr/"$(get_libdir)"/Isabelle"${PV}

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() {
	use proofgeneral && epatch ${FILESDIR}/isabelle-2009-proofgeneral-gentoo-path.patch
}

src_compile() {
	einfo "Building Isabelle logics. This may take some time."
	./build -b || die "building logics failed"
	if use graphbrowsing
	then
		cd lib/browser
		emake clean || die "failed cleaning graph browser directory"
		emake || die "failed building the graph browser"
	fi
}

src_test() {
	einfo "Running tests. A test run can take up to several hours!"
	./build -b HOL -t
}

src_install() {
	exeinto ${TARGETDIR}/bin
	doexe bin/isabelle-process bin/isabelle \
		|| die "install failed"

	exeinto ${TARGETDIR}
	doexe build || die "install failed"

	insinto ${TARGETDIR}
	use doc && ( doins -r doc || die "install failed" )

	doins -r etc || die "install failed"
	dosym ${LIBDIR}/heaps ${TARGETDIR}/heaps

	insinto ${LIBDIR}
	doins -r heaps || die "install failed"

	# use cp to keep file attributes
	cp -R lib ${D}${TARGETDIR} || die "install failed"

	bin/isabelle install -d ${TARGETDIR} -p ${D}usr/bin
	newicon lib/icons/isabelle.xpm ${PN}.xpm
	dodoc ANNOUNCE CONTRIBUTORS INSTALL NEWS README \
		|| die "dodoc failed"
}

pkg_postinst() {
	elog "You will need to re-emerge Isabelle after emerging polyml."
}