# HG changeset patch
# User blanchet
# Date 1411986609 -7200
# Node ID d15707791817923407edad93b0b73e952d8d13e6
# Parent  999adf103930577e762e40a3865acf2b880c7506# Parent  ab4b94892c4cc64f5a74971a06f63208b5a286cd
merge

diff -r 999adf103930 -r d15707791817 Admin/isatest/isatest-makedist
--- a/Admin/isatest/isatest-makedist	Mon Sep 29 12:29:52 2014 +0200
+++ b/Admin/isatest/isatest-makedist	Mon Sep 29 12:30:09 2014 +0200
@@ -104,12 +104,11 @@
 sleep 15
 $SSH lxbroy4 "
   $MAKEALL $HOME/settings/at-poly;
+  $MAKEALL $HOME/settings/at-poly-e;
   $MAKEALL $HOME/settings/at-poly-test"
 sleep 15
 $SSH lxbroy3 "$MAKEALL -l HOL-Library $HOME/settings/at-sml-dev-e"
 sleep 15
-$SSH macbroy23 "$MAKEALL $HOME/settings/at-poly-e"
-sleep 15
 $SSH macbroy2 "
   $MAKEALL $HOME/settings/mac-poly64-M4;
   $MAKEALL $HOME/settings/mac-poly64-M8;
diff -r 999adf103930 -r d15707791817 lib/scripts/run-polyml-5.5.3
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/run-polyml-5.5.3	Mon Sep 29 12:30:09 2014 +0200
@@ -0,0 +1,90 @@
+#!/usr/bin/env bash
+# :mode=shellscript:
+#
+# Author: Makarius
+#
+# Startup script for Poly/ML 5.5.3.
+
+export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
+
+
+## diagnostics
+
+function fail()
+{
+  echo "$1" >&2
+  exit 2
+}
+
+function fail_out()
+{
+  fail "Unable to create output heap file: \"$OUTFILE\""
+}
+
+function check_file()
+{
+  [ ! -f "$1" ] && fail "Unable to locate \"$1\""
+}
+
+
+## compiler executables and libraries
+
+[ -z "$ML_HOME" ] && fail "Missing ML installation (ML_HOME)"
+
+POLY="$ML_HOME/poly"
+check_file "$POLY"
+
+librarypath "$ML_HOME"
+
+
+
+## prepare databases
+
+if [ -z "$INFILE" ]; then
+  INIT=""
+  EXIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
+else
+  check_file "$INFILE"
+  INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$INFILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $INFILE\\n\"); Posix.Process.exit 0w1));"
+  EXIT=""
+fi
+
+if [ -z "$OUTFILE" ]; then
+  COMMIT='fun commit () = false;'
+  MLEXIT=""
+else
+  if [ -z "$INFILE" ]; then
+    COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); Posix.Process.exit 0w1);"
+  else
+    COMMIT="fun commit () = (ML_System.share_common_data (); ML_System.save_state \"$OUTFILE\");"
+  fi
+  [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
+  MLEXIT="commit();"
+fi
+
+
+## run it!
+
+MLTEXT="$INIT $EXIT $COMMIT $MLTEXT"
+
+if [ -n "$TERMINATE" -a -z "$MLEXIT" ]; then
+  "$POLY" -q -i $ML_OPTIONS --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")" \
+    --error-exit </dev/null
+  RC="$?"
+else
+  if [ -z "$TERMINATE" ]; then
+    FEEDER_OPTS=""
+  else
+    FEEDER_OPTS="-q"
+    ML_OPTIONS="$ML_OPTIONS --error-exit"
+  fi
+  "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
+    { read FPID; "$POLY" -q -i $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
+  RC="$?"
+fi
+
+[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
+
+exit "$RC"
+
+#:wrap=soft:maxLineLen=100:
diff -r 999adf103930 -r d15707791817 src/Pure/ML-Systems/polyml-5.5.3.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/polyml-5.5.3.ML	Mon Sep 29 12:30:09 2014 +0200
@@ -0,0 +1,23 @@
+(*  Title:      Pure/ML-Systems/polyml-5.5.3.ML
+    Author:     Makarius
+
+Compatibility wrapper for Poly/ML 5.5.3.
+*)
+
+structure Thread =
+struct
+  open Thread;
+
+  structure Thread =
+  struct
+    open Thread;
+
+    fun numProcessors () =
+      (case Thread.numPhysicalProcessors () of
+        SOME n => n
+      | NONE => Thread.numProcessors ());
+  end;
+end;
+
+use "ML-Systems/polyml.ML";
+
diff -r 999adf103930 -r d15707791817 src/Pure/ROOT
--- a/src/Pure/ROOT	Mon Sep 29 12:29:52 2014 +0200
+++ b/src/Pure/ROOT	Mon Sep 29 12:30:09 2014 +0200
@@ -14,6 +14,7 @@
     "ML-Systems/overloading_smlnj.ML"
     "ML-Systems/polyml.ML"
     "ML-Systems/polyml-5.5.2.ML"
+    "ML-Systems/polyml-5.5.3.ML"
     "ML-Systems/pp_dummy.ML"
     "ML-Systems/proper_int.ML"
     "ML-Systems/single_assignment.ML"
@@ -39,6 +40,7 @@
     "ML-Systems/overloading_smlnj.ML"
     "ML-Systems/polyml.ML"
     "ML-Systems/polyml-5.5.2.ML"
+    "ML-Systems/polyml-5.5.3.ML"
     "ML-Systems/pp_dummy.ML"
     "ML-Systems/proper_int.ML"
     "ML-Systems/single_assignment.ML"
diff -r 999adf103930 -r d15707791817 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Mon Sep 29 12:29:52 2014 +0200
+++ b/src/Pure/ROOT.ML	Mon Sep 29 12:30:09 2014 +0200
@@ -96,12 +96,14 @@
 
 if ML_System.name = "polyml-5.5.1"
   orelse ML_System.name = "polyml-5.5.2"
+  orelse ML_System.name = "polyml-5.5.3"
 then use "ML/exn_trace_polyml-5.5.1.ML"
 else ();
 
 if ML_System.name = "polyml-5.5.0"
   orelse ML_System.name = "polyml-5.5.1"
   orelse ML_System.name = "polyml-5.5.2"
+  orelse ML_System.name = "polyml-5.5.3"
 then use "ML/ml_statistics_polyml-5.5.0.ML"
 else use "ML/ml_statistics_dummy.ML";