From 10e215a3ae1fc282809356f45c78ffece4525da7 Mon Sep 17 00:00:00 2001
From: John Wiegley <johnw@newartisans.com>
Date: Tue, 30 Sep 2014 23:11:26 -0500
Subject: [PATCH] isabelle: Version 2014 building on Linux and Darwin

---
 pkgs/applications/science/logic/isabelle/default.nix | 11 ++++++++---
 pkgs/development/compilers/polyml/default.nix        |  4 ++--
 pkgs/top-level/all-packages.nix                      |  1 +
 3 files changed, 11 insertions(+), 5 deletions(-)

diff --git a/pkgs/applications/science/logic/isabelle/default.nix b/pkgs/applications/science/logic/isabelle/default.nix
index 9659ee229307..88bbe820e2f3 100644
--- a/pkgs/applications/science/logic/isabelle/default.nix
+++ b/pkgs/applications/science/logic/isabelle/default.nix
@@ -1,4 +1,4 @@
-{ stdenv, fetchurl, perl, nettools, polyml, proofgeneral }:
+{ stdenv, fetchurl, perl, nettools, java, polyml, proofgeneral }:
 # nettools needed for hostname
 
 let
@@ -21,7 +21,7 @@ stdenv.mkDerivation {
     };
 
   buildInputs = [ perl polyml ]
-             ++ stdenv.lib.optional (!stdenv.isDarwin) nettools;
+             ++ stdenv.lib.optionals (!stdenv.isDarwin) [ nettools java ];
 
   sourceRoot = dirname;
 
@@ -35,10 +35,15 @@ stdenv.mkDerivation {
     substituteInPlace etc/settings \
       --subst-var-by ML_HOME "${polyml}/bin" \
       --subst-var-by PROOFGENERAL_HOME "${proofgeneral}/share/emacs/site-lisp/ProofGeneral"
+    substituteInPlace contrib/jdk/etc/settings \
+      --replace ISABELLE_JDK_HOME= '#ISABELLE_JDK_HOME='
+    substituteInPlace contrib/polyml-5.5.2-1/etc/settings \
+      --replace 'ML_HOME="$POLYML_HOME/$ML_PLATFORM"' \
+                "ML_HOME=\"${polyml}/bin\""
   '';
 
   buildPhase = ''
-    ./bin/isabelle build -s $theories
+    ISABELLE_JDK_HOME=${java} ./bin/isabelle build -s $theories
   '';
 
   installPhase = ''
diff --git a/pkgs/development/compilers/polyml/default.nix b/pkgs/development/compilers/polyml/default.nix
index 9c0af4ec9ab3..76bb811dd66d 100644
--- a/pkgs/development/compilers/polyml/default.nix
+++ b/pkgs/development/compilers/polyml/default.nix
@@ -1,7 +1,7 @@
 {stdenv, fetchurl}:
 
 let
-  version = "5.5.1";
+  version = "5.5.2";
 in
 
 stdenv.mkDerivation {
@@ -9,7 +9,7 @@ stdenv.mkDerivation {
 
   src = fetchurl {
     url = "mirror://sourceforge/polyml/polyml.${version}.tar.gz";
-    sha256 = "16i0ir5mydl7381aijihkll19khp3z8dq0g2ja6k0pcbpkd0k06g";
+    sha256 = "10m680qdad6bd50bav9xjsgmsxw8yxg55vr7grbg0gvykzl2pzbk";
   };
 
   meta = {
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index 8ee125fb17fe..bd19493ce3ee 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -11506,6 +11506,7 @@ let
   isabelle = import ../applications/science/logic/isabelle {
     inherit (pkgs) stdenv fetchurl nettools perl polyml;
     inherit (pkgs.emacs24Packages) proofgeneral;
+    java = if stdenv.isLinux then jre else jdk;
   };
 
   iprover = callPackage ../applications/science/logic/iprover {};