# HG changeset patch
# User wenzelm
# Date 1449439808 -3600
# Node ID 4c232a2ddeab10bf9fab64ee9af5f6c4768398cd
# Parent  4c9e1e5a240e58e83e81a6c186348fb09c84b8b7
discontinued intermediate polyml-5.5.3, assuming the coming release will be polyml-5.6;

diff -r 4c9e1e5a240e -r 4c232a2ddeab lib/scripts/run-polyml-5.5.3
--- a/lib/scripts/run-polyml-5.5.3	Sun Dec 06 17:27:42 2015 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,106 +0,0 @@
-#!/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
-
-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 4c9e1e5a240e -r 4c232a2ddeab src/Pure/ML-Systems/ml_compiler_parameters_polyml-5.5.3.ML
--- a/src/Pure/ML-Systems/ml_compiler_parameters_polyml-5.5.3.ML	Sun Dec 06 17:27:42 2015 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,12 +0,0 @@
-(*  Title:      Pure/ML/ml_compiler_parameters_polyml-5.5.3.ML
-    Author:     Makarius
-
-Additional ML compiler parameters for Poly/ML 5.5.3, or later.
-*)
-
-structure ML_Compiler_Parameters: ML_COMPILER_PARAMETERS =
-struct
-
-fun debug b = [PolyML.Compiler.CPDebug b];
-
-end;
\ No newline at end of file
diff -r 4c9e1e5a240e -r 4c232a2ddeab src/Pure/ML-Systems/ml_compiler_parameters_polyml-5.6.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/ml_compiler_parameters_polyml-5.6.ML	Sun Dec 06 23:10:08 2015 +0100
@@ -0,0 +1,12 @@
+(*  Title:      Pure/ML/ml_compiler_parameters_polyml-5.6.ML
+    Author:     Makarius
+
+Additional ML compiler parameters for Poly/ML 5.6, or later.
+*)
+
+structure ML_Compiler_Parameters: ML_COMPILER_PARAMETERS =
+struct
+
+fun debug b = [PolyML.Compiler.CPDebug b];
+
+end;
\ No newline at end of file
diff -r 4c9e1e5a240e -r 4c232a2ddeab src/Pure/ML-Systems/ml_debugger_polyml-5.5.3.ML
--- a/src/Pure/ML-Systems/ml_debugger_polyml-5.5.3.ML	Sun Dec 06 17:27:42 2015 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,70 +0,0 @@
-(*  Title:      Pure/ML/ml_debugger_polyml-5.5.3.ML
-    Author:     Makarius
-
-ML debugger interface -- for Poly/ML 5.5.3, or later.
-*)
-
-signature ML_DEBUGGER =
-sig
-  type exn_id
-  val exn_id: exn -> exn_id
-  val print_exn_id: exn_id -> string
-  val eq_exn_id: exn_id * exn_id -> bool
-  type location
-  val on_entry: (string * location -> unit) option -> unit
-  val on_exit: (string * location -> unit) option -> unit
-  val on_exit_exception: (string * location -> exn -> unit) option -> unit
-  val on_breakpoint: (location * bool Unsynchronized.ref -> unit) option -> unit
-  type state
-  val state: Thread.thread -> state list
-  val debug_function: state -> string
-  val debug_function_arg: state -> ML_Name_Space.valueVal
-  val debug_function_result: state -> ML_Name_Space.valueVal
-  val debug_location: state -> location
-  val debug_name_space: state -> ML_Name_Space.T
-end;
-
-structure ML_Debugger: ML_DEBUGGER =
-struct
-
-(* exceptions *)
-
-abstype exn_id = Exn_Id of string * int Unsynchronized.ref
-with
-
-fun exn_id exn =
-  Exn_Id (General.exnName exn, RunCall.run_call2 RuntimeCalls.POLY_SYS_load_word (exn, 0));
-
-fun print_exn_id (Exn_Id (name, _)) = name;
-fun eq_exn_id (Exn_Id (_, id1), Exn_Id (_, id2)) = PolyML.pointerEq (id1, id2);
-
-end;
-
-val _ =
-  PolyML.addPrettyPrinter (fn _ => fn _ => fn exn_id =>
-    let val s = print_exn_id exn_id
-    in ml_pretty (ML_Pretty.String (s, size s)) end);
-
-
-(* hooks *)
-
-type location = PolyML.location;
-
-val on_entry = PolyML.DebuggerInterface.setOnEntry;
-val on_exit = PolyML.DebuggerInterface.setOnExit;
-val on_exit_exception = PolyML.DebuggerInterface.setOnExitException;
-val on_breakpoint = PolyML.DebuggerInterface.setOnBreakPoint;
-
-
-(* debugger operations *)
-
-type state = PolyML.DebuggerInterface.debugState;
-
-val state = PolyML.DebuggerInterface.debugState;
-val debug_function = PolyML.DebuggerInterface.debugFunction;
-val debug_function_arg = PolyML.DebuggerInterface.debugFunctionArg;
-val debug_function_result = PolyML.DebuggerInterface.debugFunctionResult;
-val debug_location = PolyML.DebuggerInterface.debugLocation;
-val debug_name_space = PolyML.DebuggerInterface.debugNameSpace;
-
-end;
diff -r 4c9e1e5a240e -r 4c232a2ddeab src/Pure/ML-Systems/ml_debugger_polyml-5.6.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/ml_debugger_polyml-5.6.ML	Sun Dec 06 23:10:08 2015 +0100
@@ -0,0 +1,70 @@
+(*  Title:      Pure/ML-Systems/ml_debugger_polyml-5.6.ML
+    Author:     Makarius
+
+ML debugger interface -- for Poly/ML 5.6, or later.
+*)
+
+signature ML_DEBUGGER =
+sig
+  type exn_id
+  val exn_id: exn -> exn_id
+  val print_exn_id: exn_id -> string
+  val eq_exn_id: exn_id * exn_id -> bool
+  type location
+  val on_entry: (string * location -> unit) option -> unit
+  val on_exit: (string * location -> unit) option -> unit
+  val on_exit_exception: (string * location -> exn -> unit) option -> unit
+  val on_breakpoint: (location * bool Unsynchronized.ref -> unit) option -> unit
+  type state
+  val state: Thread.thread -> state list
+  val debug_function: state -> string
+  val debug_function_arg: state -> ML_Name_Space.valueVal
+  val debug_function_result: state -> ML_Name_Space.valueVal
+  val debug_location: state -> location
+  val debug_name_space: state -> ML_Name_Space.T
+end;
+
+structure ML_Debugger: ML_DEBUGGER =
+struct
+
+(* exceptions *)
+
+abstype exn_id = Exn_Id of string * int Unsynchronized.ref
+with
+
+fun exn_id exn =
+  Exn_Id (General.exnName exn, RunCall.run_call2 RuntimeCalls.POLY_SYS_load_word (exn, 0));
+
+fun print_exn_id (Exn_Id (name, _)) = name;
+fun eq_exn_id (Exn_Id (_, id1), Exn_Id (_, id2)) = PolyML.pointerEq (id1, id2);
+
+end;
+
+val _ =
+  PolyML.addPrettyPrinter (fn _ => fn _ => fn exn_id =>
+    let val s = print_exn_id exn_id
+    in ml_pretty (ML_Pretty.String (s, size s)) end);
+
+
+(* hooks *)
+
+type location = PolyML.location;
+
+val on_entry = PolyML.DebuggerInterface.setOnEntry;
+val on_exit = PolyML.DebuggerInterface.setOnExit;
+val on_exit_exception = PolyML.DebuggerInterface.setOnExitException;
+val on_breakpoint = PolyML.DebuggerInterface.setOnBreakPoint;
+
+
+(* debugger operations *)
+
+type state = PolyML.DebuggerInterface.debugState;
+
+val state = PolyML.DebuggerInterface.debugState;
+val debug_function = PolyML.DebuggerInterface.debugFunction;
+val debug_function_arg = PolyML.DebuggerInterface.debugFunctionArg;
+val debug_function_result = PolyML.DebuggerInterface.debugFunctionResult;
+val debug_location = PolyML.DebuggerInterface.debugLocation;
+val debug_name_space = PolyML.DebuggerInterface.debugNameSpace;
+
+end;
diff -r 4c9e1e5a240e -r 4c232a2ddeab src/Pure/ML-Systems/ml_parse_tree_polyml-5.5.3.ML
--- a/src/Pure/ML-Systems/ml_parse_tree_polyml-5.5.3.ML	Sun Dec 06 17:27:42 2015 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,16 +0,0 @@
-(*  Title:      Pure/ML/ml_parse_tree_polyml-5.5.3.ML
-    Author:     Makarius
-
-Additional ML parse tree components for Poly/ML 5.5.3, or later.
-*)
-
-structure ML_Parse_Tree: ML_PARSE_TREE =
-struct
-
-fun completions (PolyML.PTcompletions x) = SOME x
-  | completions _ = NONE;
-
-fun breakpoint (PolyML.PTbreakPoint x) = SOME x
-  | breakpoint _ = NONE;
-
-end;
\ No newline at end of file
diff -r 4c9e1e5a240e -r 4c232a2ddeab src/Pure/ML-Systems/ml_parse_tree_polyml-5.6.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/ml_parse_tree_polyml-5.6.ML	Sun Dec 06 23:10:08 2015 +0100
@@ -0,0 +1,16 @@
+(*  Title:      Pure/ML-Systems/ml_parse_tree_polyml-5.6.ML
+    Author:     Makarius
+
+Additional ML parse tree components for Poly/ML 5.6, or later.
+*)
+
+structure ML_Parse_Tree: ML_PARSE_TREE =
+struct
+
+fun completions (PolyML.PTcompletions x) = SOME x
+  | completions _ = NONE;
+
+fun breakpoint (PolyML.PTbreakPoint x) = SOME x
+  | breakpoint _ = NONE;
+
+end;
\ No newline at end of file
diff -r 4c9e1e5a240e -r 4c232a2ddeab src/Pure/ML-Systems/ml_stack_polyml-5.5.3.ML
--- a/src/Pure/ML-Systems/ml_stack_polyml-5.5.3.ML	Sun Dec 06 17:27:42 2015 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,16 +0,0 @@
-(*  Title:      Pure/ML-Systems/ml_stack_polyml-5.5.3.ML
-
-Maximum stack size (in words) for ML threads -- Poly/ML 5.5.3, or later.
-*)
-
-signature ML_STACK =
-sig
-  val limit: int option -> Thread.threadAttribute list
-end;
-
-structure ML_Stack: ML_STACK =
-struct
-
-fun limit m = [Thread.MaximumMLStack m];
-
-end;
diff -r 4c9e1e5a240e -r 4c232a2ddeab src/Pure/ML-Systems/ml_stack_polyml-5.6.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/ml_stack_polyml-5.6.ML	Sun Dec 06 23:10:08 2015 +0100
@@ -0,0 +1,16 @@
+(*  Title:      Pure/ML-Systems/ml_stack_polyml-5.6.ML
+
+Maximum stack size (in words) for ML threads -- Poly/ML 5.6, or later.
+*)
+
+signature ML_STACK =
+sig
+  val limit: int option -> Thread.threadAttribute list
+end;
+
+structure ML_Stack: ML_STACK =
+struct
+
+fun limit m = [Thread.MaximumMLStack m];
+
+end;
diff -r 4c9e1e5a240e -r 4c232a2ddeab src/Pure/ML-Systems/polyml-5.5.3.ML
--- a/src/Pure/ML-Systems/polyml-5.5.3.ML	Sun Dec 06 17:27:42 2015 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,23 +0,0 @@
-(*  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 4c9e1e5a240e -r 4c232a2ddeab src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Sun Dec 06 17:27:42 2015 +0100
+++ b/src/Pure/ML-Systems/polyml.ML	Sun Dec 06 23:10:08 2015 +0100
@@ -60,7 +60,6 @@
 
 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 ();
@@ -78,9 +77,8 @@
 use "ML-Systems/multithreading.ML";
 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"
+if ML_System.name = "polyml-5.6"
+then use "ML-Systems/ml_stack_polyml-5.6.ML"
 else use "ML-Systems/ml_stack_dummy.ML";
 
 use "ML-Systems/unsynchronized.ML";
@@ -176,9 +174,8 @@
 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 ();
+if ML_System.name = "polyml-5.6"
+then use "ML-Systems/ml_compiler_parameters_polyml-5.6.ML" else ();
 
 use "ML-Systems/use_context.ML";
 use "ML-Systems/ml_positions.ML";
@@ -191,9 +188,8 @@
 fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
 
 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 ();
+if ML_System.name = "polyml-5.6"
+then use "ML-Systems/ml_parse_tree_polyml-5.6.ML" else ();
 
 fun toplevel_pp context (_: string list) pp =
   use_text context {line = 1, file = "pp", verbose = false, debug = false}
@@ -206,7 +202,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"
+if ML_System.name = "polyml-5.6"
+then use "ML-Systems/ml_debugger_polyml-5.6.ML"
 else use "ML-Systems/ml_debugger.ML";
diff -r 4c9e1e5a240e -r 4c232a2ddeab src/Pure/ROOT
--- a/src/Pure/ROOT	Sun Dec 06 17:27:42 2015 +0100
+++ b/src/Pure/ROOT	Sun Dec 06 23:10:08 2015 +0100
@@ -7,26 +7,26 @@
     "ML-Systems/compiler_polyml.ML"
     "ML-Systems/exn_trace_polyml-5.5.1.ML"
     "ML-Systems/ml_compiler_parameters.ML"
-    "ML-Systems/ml_compiler_parameters_polyml-5.5.3.ML"
+    "ML-Systems/ml_compiler_parameters_polyml-5.6.ML"
     "ML-Systems/ml_debugger.ML"
-    "ML-Systems/ml_debugger_polyml-5.5.3.ML"
+    "ML-Systems/ml_debugger_polyml-5.6.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_parse_tree_polyml-5.6.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_stack_polyml-5.6.ML"
     "ML-Systems/ml_system.ML"
     "ML-Systems/multithreading.ML"
     "ML-Systems/multithreading_polyml.ML"
     "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-5.6.ML"
     "ML-Systems/polyml.ML"
     "ML-Systems/pp_dummy.ML"
@@ -48,26 +48,25 @@
     "ML-Systems/compiler_polyml.ML"
     "ML-Systems/exn_trace_polyml-5.5.1.ML"
     "ML-Systems/ml_compiler_parameters.ML"
-    "ML-Systems/ml_compiler_parameters_polyml-5.5.3.ML"
+    "ML-Systems/ml_compiler_parameters_polyml-5.6.ML"
     "ML-Systems/ml_debugger.ML"
-    "ML-Systems/ml_debugger_polyml-5.5.3.ML"
+    "ML-Systems/ml_debugger_polyml-5.6.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_parse_tree_polyml-5.6.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_stack_polyml-5.6.ML"
     "ML-Systems/ml_system.ML"
     "ML-Systems/multithreading.ML"
     "ML-Systems/multithreading_polyml.ML"
     "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"
diff -r 4c9e1e5a240e -r 4c232a2ddeab src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sun Dec 06 17:27:42 2015 +0100
+++ b/src/Pure/ROOT.ML	Sun Dec 06 23:10:08 2015 +0100
@@ -105,7 +105,6 @@
 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"
   orelse ML_System.name = "polyml-5.6"
 then use "ML/ml_statistics_polyml-5.5.0.ML"
 else use "ML/ml_statistics_dummy.ML";