# HG changeset patch
# User wenzelm
# Date 1440072780 -7200
# Node ID ff4a67c65084d9bdaa4a663a9ebd0bad22b92d2c
# Parent  67e389f67073e8c9c59bd1f46c9e65529587ca91
updated to polyml-5.5.3-20150820, with native x86-windows support;

diff -r 67e389f67073 -r ff4a67c65084 Admin/components/components.sha1
--- a/Admin/components/components.sha1	Thu Aug 20 13:41:53 2015 +0200
+++ b/Admin/components/components.sha1	Thu Aug 20 14:13:00 2015 +0200
@@ -91,6 +91,7 @@
 4b690390946f7bfb777b89eb16d6f08987cca12f  polyml-5.5.2-2.tar.gz
 5b31ad8556e41dfd6d5e85f407818be399aa3d2a  polyml-5.5.2-3.tar.gz
 532f6e8814752aeb406c62fabcfd2cc05f8a7ca8  polyml-5.5.2.tar.gz
+1c53f699d35c0db6c7cf4ea51f2310adbd1d0dc5  polyml-5.5.3-20150820.tar.gz
 8ee375cfc38972f080dbc78f07b68dac03efe968  ProofGeneral-3.7.1.1.tar.gz
 847b52c0676b5eb0fbf0476f64fc08c2d72afd0c  ProofGeneral-4.1.tar.gz
 8e0b2b432755ef11d964e20637d1bc567d1c0477  ProofGeneral-4.2-1.tar.gz
diff -r 67e389f67073 -r ff4a67c65084 Admin/components/main
--- a/Admin/components/main	Thu Aug 20 13:41:53 2015 +0200
+++ b/Admin/components/main	Thu Aug 20 14:13:00 2015 +0200
@@ -9,7 +9,7 @@
 jfreechart-1.0.14-1
 jortho-1.0-2
 kodkodi-1.5.2
-polyml-5.5.2-3
+polyml-5.5.3-20150820
 scala-2.11.7
 spass-3.8ds
 xz-java-1.2-1
diff -r 67e389f67073 -r ff4a67c65084 Admin/polyml/README
--- a/Admin/polyml/README	Thu Aug 20 13:41:53 2015 +0200
+++ b/Admin/polyml/README	Thu Aug 20 14:13:00 2015 +0200
@@ -1,12 +1,8 @@
 Poly/ML for Isabelle
 ====================
 
-This compilation of Poly/ML 5.5.2 is based on
-http://sourceforge.net/p/polyml/code/HEAD/tree/fixes-5.5.2 version
-2009.  See also fixes-5.5.2.diff for the differences to the official
-source distribution polyml.5.5.2.tar.gz from
-http://sourceforge.net/projects/polyml/.
-
+This is a preview of Poly/ML 5.5.3, based on
+https://github.com/polyml/polyml/commit/3fbfb80c471f
 
 The included build script is used like this:
 
@@ -14,11 +10,11 @@
   ./build src x86_64-linux --with-gmp
   ./build src x86-darwin --without-gmp
   ./build src x86_64-darwin --without-gmp
-  ./build src x86-cygwin --with-gmp
+  ./build src x86-windows --with-gmp
 
 Also note that the separate "sha1" library module is required for
 efficient digesting of strings according to SHA-1.
 
 
         Makarius
-        22-Apr-2015
+        20-Aug-2015
diff -r 67e389f67073 -r ff4a67c65084 Admin/polyml/polyml
--- a/Admin/polyml/polyml	Thu Aug 20 13:41:53 2015 +0200
+++ b/Admin/polyml/polyml	Thu Aug 20 14:13:00 2015 +0200
@@ -8,4 +8,3 @@
 export DYLD_LIBRARY_PATH="$THIS:$DYLD_LIBRARY_PATH"
 
 exec "$THIS/poly" "$@"
-
diff -r 67e389f67073 -r ff4a67c65084 Admin/polyml/settings
--- a/Admin/polyml/settings	Thu Aug 20 13:41:53 2015 +0200
+++ b/Admin/polyml/settings	Thu Aug 20 14:13:00 2015 +0200
@@ -3,9 +3,9 @@
 POLYML_HOME="$COMPONENT"
 
 
-# basic settings
+# simple settings (example)
 
-#ML_SYSTEM=polyml-5.5.2
+#ML_SYSTEM=polyml-5.5.3
 #ML_PLATFORM="$ISABELLE_PLATFORM32"
 #ML_HOME="$POLYML_HOME/$ML_PLATFORM"
 #ML_OPTIONS="-H 500"
@@ -14,7 +14,7 @@
 
 # smart settings
 
-ML_SYSTEM=polyml-5.5.2
+ML_SYSTEM=polyml-5.5.3
 
 case "$ISABELLE_PLATFORM" in
   *-linux)
@@ -31,6 +31,9 @@
       fi
     fi
     ;;
+  x86-cygwin)
+    ML_PLATFORM="x86-windows"
+    ;;
   *)
     ML_PLATFORM="$ISABELLE_PLATFORM32"
     ;;
@@ -47,4 +50,3 @@
 
 ML_HOME="$POLYML_HOME/$ML_PLATFORM"
 ML_SOURCES="$POLYML_HOME/src"
-
diff -r 67e389f67073 -r ff4a67c65084 NEWS
--- a/NEWS	Thu Aug 20 13:41:53 2015 +0200
+++ b/NEWS	Thu Aug 20 14:13:00 2015 +0200
@@ -286,6 +286,12 @@
 the proof context discipline.
 
 
+*** System ***
+
+* Poly/ML 5.5.3 runs natively on x86-windows, with somewhat larger heap
+space than former x86-cygwin.
+
+
 
 New in Isabelle2015 (May 2015)
 ------------------------------