# HG changeset patch
# User wenzelm
# Date 1448052725 -3600
# Node ID 5dc95d957569ef8f007a20f8a3bb6aa18b3e2dca
# Parent  7c1ad030f0c9a1991165ecb6396ac46924e247fb
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;

diff -r 7c1ad030f0c9 -r 5dc95d957569 lib/scripts/run-polyml-5.6
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/run-polyml-5.6	Fri Nov 20 21:52:05 2015 +0100
@@ -0,0 +1,106 @@
+#!/usr/bin/env bash
+# :mode=shellscript:
+#
+# Author: Makarius
+#
+# Startup script for Poly/ML 5.6.
+
+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
+
+case "$ML_PLATFORM" in
+  *-windows)
+    PLATFORM_INFILE="$(platform_path -m "$INFILE")"
+    PLATFORM_OUTFILE="$(platform_path -m "$OUTFILE")"
+    ;;
+  *)
+    PLATFORM_INFILE="$INFILE"
+    PLATFORM_OUTFILE="$OUTFILE"
+    ;;
+esac
+
+if [ -z "$INFILE" ]; then
+  INIT=""
+  case "$ML_PLATFORM" in
+    *-windows)
+      EXIT="fun exit 0 = OS.Process.exit OS.Process.success | exit 1 = OS.Process.exit OS.Process.failure | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc));"
+      ;;
+    *)
+      EXIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
+      ;;
+  esac
+else
+  check_file "$INFILE"
+  INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$PLATFORM_INFILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $INFILE\\n\"); OS.Process.exit OS.Process.success));"
+  EXIT=""
+fi
+
+if [ -z "$OUTFILE" ]; then
+  MLEXIT=""
+else
+  if [ -z "$INFILE" ]; then
+    MLEXIT="(PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$PLATFORM_OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); OS.Process.exit OS.Process.success);"
+  else
+    MLEXIT="Session.save \"$OUTFILE\";"
+  fi
+  [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
+fi
+
+
+## run it!
+
+MLTEXT="$INIT $EXIT $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 7c1ad030f0c9 -r 5dc95d957569 src/Pure/ML-Systems/ml_name_space_polyml-5.6.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/ml_name_space_polyml-5.6.ML	Fri Nov 20 21:52:05 2015 +0100
@@ -0,0 +1,33 @@
+(*  Title:      Pure/ML-Systems/ml_name_space_polyml-5.6.ML
+    Author:     Makarius
+
+Name space for Poly/ML.
+*)
+
+structure ML_Name_Space =
+struct
+  open PolyML.NameSpace;
+
+  type T = PolyML.NameSpace.nameSpace;
+  val global = PolyML.globalNameSpace;
+  val forget_global_structure = PolyML.Compiler.forgetStructure;
+
+  type valueVal = Values.value;
+  fun displayVal (x, depth, space) = Values.printWithType (x, depth, SOME space);
+  fun displayTypeExpression (x, depth, space) = Values.printType (x, depth, SOME space);
+
+  type typeVal = TypeConstrs.typeConstr;
+  fun displayType (x, depth, space) = TypeConstrs.print (x, depth, SOME space);
+
+  type fixityVal = Infixes.fixity;
+  fun displayFix (_: string, x) = Infixes.print x;
+
+  type structureVal = Structures.structureVal;
+  fun displayStruct (x, depth, space) = Structures.print (x, depth, SOME space);
+
+  type signatureVal = Signatures.signatureVal;
+  fun displaySig (x, depth, space) = Signatures.print (x, depth, SOME space);
+
+  type functorVal = Functors.functorVal;
+  fun displayFunct (x, depth, space) = Functors.print (x, depth, SOME space);
+end;
diff -r 7c1ad030f0c9 -r 5dc95d957569 src/Pure/ML-Systems/ml_name_space_polyml.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/ml_name_space_polyml.ML	Fri Nov 20 21:52:05 2015 +0100
@@ -0,0 +1,13 @@
+(*  Title:      Pure/ML-Systems/ml_name_space_polyml.ML
+    Author:     Makarius
+
+Name space for Poly/ML.
+*)
+
+structure ML_Name_Space =
+struct
+  open PolyML.NameSpace;
+  type T = nameSpace;
+  val global = PolyML.globalNameSpace;
+  val forget_global_structure = PolyML.Compiler.forgetStructure;
+end;
diff -r 7c1ad030f0c9 -r 5dc95d957569 src/Pure/ML-Systems/ml_profiling_polyml-5.6.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/ml_profiling_polyml-5.6.ML	Fri Nov 20 21:52:05 2015 +0100
@@ -0,0 +1,17 @@
+(*  Title:      Pure/ML-Systems/ml_profiling_polyml-5.6.ML
+    Author:     Makarius
+
+Profiling for Poly/ML 5.6.
+*)
+
+fun profile 0 f x = f x
+  | profile n f x =
+      let
+        val mode =
+          (case n of
+            1 => PolyML.Profiling.ProfileTime
+          | 2 => PolyML.Profiling.ProfileAllocations
+          | 3 => PolyML.Profiling.ProfileLongIntEmulation
+          | 6 => PolyML.Profiling.ProfileTimeThisThread
+          | _ => raise Fail ("Bad profile mode: " ^ Int.toString n));
+      in PolyML.Profiling.profile mode f x end;
diff -r 7c1ad030f0c9 -r 5dc95d957569 src/Pure/ML-Systems/ml_profiling_polyml.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/ml_profiling_polyml.ML	Fri Nov 20 21:52:05 2015 +0100
@@ -0,0 +1,13 @@
+(*  Title:      Pure/ML-Systems/ml_profiling_polyml.ML
+    Author:     Makarius
+
+Profiling for Poly/ML.
+*)
+
+fun profile 0 f x = f x
+  | profile n f x =
+      let
+        val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler n;
+        val res = Exn.capture f x;
+        val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0;
+      in Exn.release res end;
diff -r 7c1ad030f0c9 -r 5dc95d957569 src/Pure/ML-Systems/polyml-5.6.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/polyml-5.6.ML	Fri Nov 20 21:52:05 2015 +0100
@@ -0,0 +1,22 @@
+(*  Title:      Pure/ML-Systems/polyml-5.6.ML
+    Author:     Makarius
+
+Compatibility wrapper for Poly/ML 5.6.
+*)
+
+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 7c1ad030f0c9 -r 5dc95d957569 src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Fri Nov 20 15:54:46 2015 +0000
+++ b/src/Pure/ML-Systems/polyml.ML	Fri Nov 20 21:52:05 2015 +0100
@@ -6,11 +6,15 @@
 
 (* initial ML name space *)
 
+use "ML-Systems/ml_system.ML";
+
+if ML_System.name = "polyml-5.6"
+then use "ML-Systems/ml_name_space_polyml-5.6.ML"
+else use "ML-Systems/ml_name_space_polyml.ML";
+
 structure ML_Name_Space =
 struct
-  open PolyML.NameSpace;
-  type T = PolyML.NameSpace.nameSpace;
-  val global = PolyML.globalNameSpace;
+  open ML_Name_Space;
   val initial_val =
     List.filter (fn (a, _) => a <> "use" andalso a <> "exit" andalso a <> "commit")
       (#allVal global ());
@@ -19,14 +23,11 @@
   val initial_structure = #allStruct global ();
   val initial_signature = #allSig global ();
   val initial_functor = #allFunct global ();
-  val forget_global_structure = PolyML.Compiler.forgetStructure;
 end;
 
 
 (* ML system operations *)
 
-use "ML-Systems/ml_system.ML";
-
 if ML_System.name = "polyml-5.3.0"
 then use "ML-Systems/share_common_data_polyml-5.3.0.ML"
 else ();
@@ -60,6 +61,7 @@
 if ML_System.name = "polyml-5.5.1"
   orelse ML_System.name = "polyml-5.5.2"
   orelse ML_System.name = "polyml-5.5.3"
+  orelse ML_System.name = "polyml-5.6"
 then use "ML-Systems/exn_trace_polyml-5.5.1.ML"
 else ();
 
@@ -77,6 +79,7 @@
 use "ML-Systems/multithreading_polyml.ML";
 
 if ML_System.name = "polyml-5.5.3"
+  orelse ML_System.name = "polyml-5.6"
 then use "ML-Systems/ml_stack_polyml-5.5.3.ML"
 else use "ML-Systems/ml_stack_dummy.ML";
 
@@ -108,16 +111,9 @@
 
 (* ML runtime system *)
 
-val timing = PolyML.timing;
-val profiling = PolyML.profiling;
-
-fun profile 0 f x = f x
-  | profile n f x =
-      let
-        val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler n;
-        val res = Exn.capture f x;
-        val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0;
-      in Exn.release res end;
+if ML_System.name = "polyml-5.6"
+then use "ML-Systems/ml_profiling_polyml-5.6.ML"
+else use "ML-Systems/ml_profiling_polyml.ML";
 
 val pointer_eq = PolyML.pointerEq;
 
@@ -176,11 +172,12 @@
 structure ML_Name_Space =
 struct
   open ML_Name_Space;
-  val display_val = pretty_ml o PolyML.NameSpace.displayVal;
+  val display_val = pretty_ml o displayVal;
 end;
 
 use "ML-Systems/ml_compiler_parameters.ML";
 if ML_System.name = "polyml-5.5.3"
+  orelse ML_System.name = "polyml-5.6"
 then use "ML-Systems/ml_compiler_parameters_polyml-5.5.3.ML" else ();
 
 use "ML-Systems/use_context.ML";
@@ -195,6 +192,7 @@
 
 use "ML-Systems/ml_parse_tree.ML";
 if ML_System.name = "polyml-5.5.3"
+  orelse ML_System.name = "polyml-5.6"
 then use "ML-Systems/ml_parse_tree_polyml-5.5.3.ML" else ();
 
 fun toplevel_pp context (_: string list) pp =
@@ -209,5 +207,6 @@
 (* ML debugger *)
 
 if ML_System.name = "polyml-5.5.3"
+  orelse ML_System.name = "polyml-5.6"
 then use "ML-Systems/ml_debugger_polyml-5.5.3.ML"
 else use "ML-Systems/ml_debugger.ML";
diff -r 7c1ad030f0c9 -r 5dc95d957569 src/Pure/ML/ml_compiler_polyml.ML
--- a/src/Pure/ML/ml_compiler_polyml.ML	Fri Nov 20 15:54:46 2015 +0000
+++ b/src/Pure/ML/ml_compiler_polyml.ML	Fri Nov 20 21:52:05 2015 +0100
@@ -39,7 +39,7 @@
         is_reported pos ?
           let
             val xml =
-              PolyML.NameSpace.displayTypeExpression (types, depth, space)
+              ML_Name_Space.displayTypeExpression (types, depth, space)
               |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
               |> Output.output |> YXML.parse_body;
           in cons (pos, fn () => Markup.ML_typing, fn () => YXML.string_of_body xml) end
@@ -188,17 +188,17 @@
           else ();
 
         fun apply_fix (a, b) =
-          (#enterFix space (a, b); display PolyML.NameSpace.displayFix (a, b));
+          (#enterFix space (a, b); display ML_Name_Space.displayFix (a, b));
         fun apply_type (a, b) =
-          (#enterType space (a, b); display PolyML.NameSpace.displayType (b, depth, space));
+          (#enterType space (a, b); display ML_Name_Space.displayType (b, depth, space));
         fun apply_sig (a, b) =
-          (#enterSig space (a, b); display PolyML.NameSpace.displaySig (b, depth, space));
+          (#enterSig space (a, b); display ML_Name_Space.displaySig (b, depth, space));
         fun apply_struct (a, b) =
-          (#enterStruct space (a, b); display PolyML.NameSpace.displayStruct (b, depth, space));
+          (#enterStruct space (a, b); display ML_Name_Space.displayStruct (b, depth, space));
         fun apply_funct (a, b) =
-          (#enterFunct space (a, b); display PolyML.NameSpace.displayFunct (b, depth, space));
+          (#enterFunct space (a, b); display ML_Name_Space.displayFunct (b, depth, space));
         fun apply_val (a, b) =
-          (#enterVal space (a, b); display PolyML.NameSpace.displayVal (b, depth, space));
+          (#enterVal space (a, b); display ML_Name_Space.displayVal (b, depth, space));
       in
         List.app apply_fix fixes;
         List.app apply_type types;
diff -r 7c1ad030f0c9 -r 5dc95d957569 src/Pure/ROOT
--- a/src/Pure/ROOT	Fri Nov 20 15:54:46 2015 +0000
+++ b/src/Pure/ROOT	Fri Nov 20 21:52:05 2015 +0100
@@ -11,10 +11,14 @@
     "ML-Systems/ml_debugger.ML"
     "ML-Systems/ml_debugger_polyml-5.5.3.ML"
     "ML-Systems/ml_name_space.ML"
+    "ML-Systems/ml_name_space_polyml-5.6.ML"
+    "ML-Systems/ml_name_space_polyml.ML"
     "ML-Systems/ml_parse_tree.ML"
     "ML-Systems/ml_parse_tree_polyml-5.5.3.ML"
     "ML-Systems/ml_positions.ML"
     "ML-Systems/ml_pretty.ML"
+    "ML-Systems/ml_profiling_polyml-5.6.ML"
+    "ML-Systems/ml_profiling_polyml.ML"
     "ML-Systems/ml_stack_dummy.ML"
     "ML-Systems/ml_stack_polyml-5.5.3.ML"
     "ML-Systems/ml_system.ML"
@@ -23,6 +27,7 @@
     "ML-Systems/overloading_smlnj.ML"
     "ML-Systems/polyml-5.5.2.ML"
     "ML-Systems/polyml-5.5.3.ML"
+    "ML-Systems/polyml-5.6.ML"
     "ML-Systems/polyml.ML"
     "ML-Systems/pp_dummy.ML"
     "ML-Systems/proper_int.ML"
@@ -47,10 +52,14 @@
     "ML-Systems/ml_debugger.ML"
     "ML-Systems/ml_debugger_polyml-5.5.3.ML"
     "ML-Systems/ml_name_space.ML"
+    "ML-Systems/ml_name_space_polyml-5.6.ML"
+    "ML-Systems/ml_name_space_polyml.ML"
     "ML-Systems/ml_parse_tree.ML"
     "ML-Systems/ml_parse_tree_polyml-5.5.3.ML"
     "ML-Systems/ml_positions.ML"
     "ML-Systems/ml_pretty.ML"
+    "ML-Systems/ml_profiling_polyml-5.6.ML"
+    "ML-Systems/ml_profiling_polyml.ML"
     "ML-Systems/ml_stack_dummy.ML"
     "ML-Systems/ml_stack_polyml-5.5.3.ML"
     "ML-Systems/ml_system.ML"
@@ -59,6 +68,7 @@
     "ML-Systems/overloading_smlnj.ML"
     "ML-Systems/polyml-5.5.2.ML"
     "ML-Systems/polyml-5.5.3.ML"
+    "ML-Systems/polyml-5.6.ML"
     "ML-Systems/polyml.ML"
     "ML-Systems/pp_dummy.ML"
     "ML-Systems/proper_int.ML"
diff -r 7c1ad030f0c9 -r 5dc95d957569 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Fri Nov 20 15:54:46 2015 +0000
+++ b/src/Pure/ROOT.ML	Fri Nov 20 21:52:05 2015 +0100
@@ -106,6 +106,7 @@
   orelse ML_System.name = "polyml-5.5.1"
   orelse ML_System.name = "polyml-5.5.2"
   orelse ML_System.name = "polyml-5.5.3"
+  orelse ML_System.name = "polyml-5.6"
 then use "ML/ml_statistics_polyml-5.5.0.ML"
 else use "ML/ml_statistics_dummy.ML";