discontinued polyml-5.3.0;
authorwenzelm
Thu Mar 03 11:12:02 2016 +0100 (2016-03-03)
changeset 6250198fa1f9a292f
parent 62498 5dfcc9697f29
child 62502 8857237c3a90
discontinued polyml-5.3.0;
Admin/Release/CHECKLIST
Admin/isatest/settings/at-poly
NEWS
lib/scripts/run-polyml-5.3.0
src/Pure/Concurrent/standard_thread.ML
src/Pure/ML/ml_compiler.ML
src/Pure/RAW/ROOT_polyml-5.6.ML
src/Pure/RAW/ROOT_polyml.ML
src/Pure/RAW/exn_trace_raw.ML
src/Pure/RAW/ml_compiler0.ML
src/Pure/RAW/ml_compiler_parameters.ML
src/Pure/RAW/ml_compiler_parameters_polyml-5.6.ML
src/Pure/RAW/ml_debugger.ML
src/Pure/RAW/ml_debugger_polyml-5.6.ML
src/Pure/RAW/ml_heap_polyml-5.3.0.ML
src/Pure/RAW/ml_name_space.ML
src/Pure/RAW/ml_name_space_polyml-5.6.ML
src/Pure/RAW/ml_name_space_polyml.ML
src/Pure/RAW/ml_parse_tree.ML
src/Pure/RAW/ml_parse_tree_polyml-5.6.ML
src/Pure/RAW/ml_profiling.ML
src/Pure/RAW/ml_profiling_polyml-5.6.ML
src/Pure/RAW/ml_profiling_polyml.ML
src/Pure/RAW/ml_stack_dummy.ML
src/Pure/RAW/ml_stack_polyml-5.6.ML
src/Pure/RAW/multithreading.ML
src/Pure/RAW/single_assignment_polyml.ML
src/Pure/ROOT
src/Pure/ROOT.ML
src/Pure/System/system_channel.ML
     1.1 --- a/Admin/Release/CHECKLIST	Wed Mar 02 19:43:31 2016 +0100
     1.2 +++ b/Admin/Release/CHECKLIST	Thu Mar 03 11:12:02 2016 +0100
     1.3 @@ -5,8 +5,6 @@
     1.4  
     1.5  - check Admin/components;
     1.6  
     1.7 -- test polyml-5.3.0;
     1.8 -
     1.9  - test 'display_drafts' command;
    1.10  
    1.11  - test "#!/usr/bin/env isabelle_scala_script";
     2.1 --- a/Admin/isatest/settings/at-poly	Wed Mar 02 19:43:31 2016 +0100
     2.2 +++ b/Admin/isatest/settings/at-poly	Thu Mar 03 11:12:02 2016 +0100
     2.3 @@ -2,11 +2,7 @@
     2.4  
     2.5  init_components /home/isabelle/contrib "$HOME/admin/components/main"
     2.6  
     2.7 -  POLYML_HOME="/home/polyml/polyml-5.3.0"
     2.8 -  ML_SYSTEM="polyml-5.3.0"
     2.9 -  ML_PLATFORM="x86-linux"
    2.10 -  ML_HOME="$POLYML_HOME/$ML_PLATFORM"
    2.11 -  ML_OPTIONS="-H 1000"
    2.12 +ML_OPTIONS="-H 1000 --gcthreads 1"
    2.13  
    2.14  ISABELLE_GHC=/usr/bin/ghc
    2.15  
    2.16 @@ -35,4 +31,3 @@
    2.17  ISABELLE_POLYML="$ML_HOME/poly"
    2.18  ISABELLE_SCALA="$SCALA_HOME/bin"
    2.19  ISABELLE_SMLNJ="/home/smlnj/bin/sml"
    2.20 -
     3.1 --- a/NEWS	Wed Mar 02 19:43:31 2016 +0100
     3.2 +++ b/NEWS	Thu Mar 03 11:12:02 2016 +0100
     3.3 @@ -205,7 +205,7 @@
     3.4  discontinued. INCOMPATIBILITY, use operations from the modules "XML" and
     3.5  "YXML" in Isabelle/ML or Isabelle/Scala.
     3.6  
     3.7 -* SML/NJ is no longer supported.
     3.8 +* SML/NJ and old versions of Poly/ML are no longer supported.
     3.9  
    3.10  
    3.11  New in Isabelle2016 (February 2016)
     4.1 --- a/lib/scripts/run-polyml-5.3.0	Wed Mar 02 19:43:31 2016 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,53 +0,0 @@
     4.4 -#!/usr/bin/env bash
     4.5 -#
     4.6 -# Author: Makarius
     4.7 -#
     4.8 -# Startup script for Poly/ML 5.3.0.
     4.9 -
    4.10 -export -n HEAP_FILE ML_TEXT TERMINATE
    4.11 -
    4.12 -
    4.13 -## diagnostics
    4.14 -
    4.15 -function fail()
    4.16 -{
    4.17 -  echo "$1" >&2
    4.18 -  exit 2
    4.19 -}
    4.20 -
    4.21 -function check_file()
    4.22 -{
    4.23 -  [ ! -f "$1" ] && fail "Unable to locate \"$1\""
    4.24 -}
    4.25 -
    4.26 -
    4.27 -## prepare databases
    4.28 -
    4.29 -if [ -z "$HEAP_FILE" ]; then
    4.30 -  INIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
    4.31 -else
    4.32 -  check_file "$HEAP_FILE"
    4.33 -  INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$HEAP_FILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $HEAP_FILE\\n\"); Posix.Process.exit 0w1));"
    4.34 -fi
    4.35 -
    4.36 -
    4.37 -## poly process
    4.38 -
    4.39 -ML_TEXT="$INIT $ML_TEXT"
    4.40 -
    4.41 -check_file "$ML_HOME/poly"
    4.42 -librarypath "$ML_HOME"
    4.43 -
    4.44 -if [ -z "$TERMINATE" ]; then
    4.45 -  FEEDER_OPTS=""
    4.46 -else
    4.47 -  FEEDER_OPTS="-q"
    4.48 -fi
    4.49 -
    4.50 -"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$ML_TEXT" $FEEDER_OPTS | \
    4.51 -  { read FPID; "$ML_HOME/poly" -q $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
    4.52 -RC="$?"
    4.53 -
    4.54 -exit "$RC"
    4.55 -
    4.56 -#:wrap=soft:maxLineLen=100:
     5.1 --- a/src/Pure/Concurrent/standard_thread.ML	Wed Mar 02 19:43:31 2016 +0100
     5.2 +++ b/src/Pure/Concurrent/standard_thread.ML	Thu Mar 03 11:12:02 2016 +0100
     5.3 @@ -49,7 +49,7 @@
     5.4  type params = {name: string, stack_limit: int option, interrupts: bool};
     5.5  
     5.6  fun attributes ({stack_limit, interrupts, ...}: params) =
     5.7 -  ML_Stack.limit stack_limit @
     5.8 +  Thread.MaximumMLStack stack_limit ::
     5.9    (if interrupts then Multithreading.public_interrupts else Multithreading.no_interrupts);
    5.10  
    5.11  fun fork (params: params) body =
     6.1 --- a/src/Pure/ML/ml_compiler.ML	Wed Mar 02 19:43:31 2016 +0100
     6.2 +++ b/src/Pure/ML/ml_compiler.ML	Thu Mar 03 11:12:02 2016 +0100
     6.3 @@ -98,10 +98,8 @@
     6.4        | reported loc (PolyML.PTdeclaredAt decl) = reported_entity Markup.ML_defN loc decl
     6.5        | reported loc (PolyML.PTopenedAt decl) = reported_entity Markup.ML_openN loc decl
     6.6        | reported loc (PolyML.PTstructureAt decl) = reported_entity Markup.ML_structureN loc decl
     6.7 -      | reported loc pt =
     6.8 -          (case ML_Parse_Tree.completions pt of
     6.9 -            SOME names => reported_completions loc names
    6.10 -          | NONE => I)
    6.11 +      | reported loc (PolyML.PTcompletions names) = reported_completions loc names
    6.12 +      | reported _ _ = I
    6.13      and reported_tree (loc, props) = fold (reported loc) props;
    6.14  
    6.15      val persistent_reports = reported_tree parse_tree [];
    6.16 @@ -123,16 +121,14 @@
    6.17  
    6.18      fun breakpoints _ (PolyML.PTnextSibling tree) = breakpoints_tree (tree ())
    6.19        | breakpoints _ (PolyML.PTfirstChild tree) = breakpoints_tree (tree ())
    6.20 -      | breakpoints loc pt =
    6.21 -          (case ML_Parse_Tree.breakpoint pt of
    6.22 -            SOME b =>
    6.23 -              let val pos = breakpoint_position loc in
    6.24 -                if is_reported pos then
    6.25 -                  let val id = serial ();
    6.26 -                  in cons ((pos, Markup.ML_breakpoint id), (id, (b, pos))) end
    6.27 -                else I
    6.28 -              end
    6.29 -          | NONE => I)
    6.30 +      | breakpoints loc (PolyML.PTbreakPoint b) =
    6.31 +          let val pos = breakpoint_position loc in
    6.32 +            if is_reported pos then
    6.33 +              let val id = serial ();
    6.34 +              in cons ((pos, Markup.ML_breakpoint id), (id, (b, pos))) end
    6.35 +            else I
    6.36 +          end
    6.37 +      | breakpoints _ _ = I
    6.38      and breakpoints_tree (loc, props) = fold (breakpoints loc) props;
    6.39  
    6.40      val all_breakpoints = rev (breakpoints_tree parse_tree []);
    6.41 @@ -264,8 +260,8 @@
    6.42        PolyML.Compiler.CPFileName location_props,
    6.43        PolyML.Compiler.CPPrintDepth ML_Options.get_print_depth,
    6.44        PolyML.Compiler.CPCompilerResultFun result_fun,
    6.45 -      PolyML.Compiler.CPPrintInAlphabeticalOrder false] @
    6.46 -     ML_Compiler_Parameters.debug debug;
    6.47 +      PolyML.Compiler.CPPrintInAlphabeticalOrder false,
    6.48 +      PolyML.Compiler.CPDebug debug];
    6.49  
    6.50      val _ =
    6.51        (while not (List.null (! input_buffer)) do
     7.1 --- a/src/Pure/RAW/ROOT_polyml-5.6.ML	Wed Mar 02 19:43:31 2016 +0100
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,22 +0,0 @@
     7.4 -(*  Title:      Pure/RAW/ROOT_polyml-5.6.ML
     7.5 -    Author:     Makarius
     7.6 -
     7.7 -Compatibility wrapper for Poly/ML 5.6.
     7.8 -*)
     7.9 -
    7.10 -structure Thread =
    7.11 -struct
    7.12 -  open Thread;
    7.13 -
    7.14 -  structure Thread =
    7.15 -  struct
    7.16 -    open Thread;
    7.17 -
    7.18 -    fun numProcessors () =
    7.19 -      (case Thread.numPhysicalProcessors () of
    7.20 -        SOME n => n
    7.21 -      | NONE => Thread.numProcessors ());
    7.22 -  end;
    7.23 -end;
    7.24 -
    7.25 -use "RAW/ROOT_polyml.ML";
     8.1 --- a/src/Pure/RAW/ROOT_polyml.ML	Wed Mar 02 19:43:31 2016 +0100
     8.2 +++ b/src/Pure/RAW/ROOT_polyml.ML	Thu Mar 03 11:12:02 2016 +0100
     8.3 @@ -7,10 +7,7 @@
     8.4  (* initial ML name space *)
     8.5  
     8.6  use "RAW/ml_system.ML";
     8.7 -
     8.8 -if ML_System.name = "polyml-5.6"
     8.9 -then use "RAW/ml_name_space_polyml-5.6.ML"
    8.10 -else use "RAW/ml_name_space_polyml.ML";
    8.11 +use "RAW/ml_name_space.ML";
    8.12  
    8.13  if List.exists (fn (a, _) => a = "FixedInt") (#allStruct ML_Name_Space.global ()) then ()
    8.14  else use "RAW/fixed_int_dummy.ML";
    8.15 @@ -29,13 +26,6 @@
    8.16  end;
    8.17  
    8.18  
    8.19 -(* ML heap operations *)
    8.20 -
    8.21 -if ML_System.name = "polyml-5.3.0"
    8.22 -then use "RAW/ml_heap_polyml-5.3.0.ML"
    8.23 -else use "RAW/ml_heap.ML";
    8.24 -
    8.25 -
    8.26  (* exceptions *)
    8.27  
    8.28  fun reraise exn =
    8.29 @@ -46,27 +36,16 @@
    8.30  exception Interrupt = SML90.Interrupt;
    8.31  
    8.32  use "RAW/exn.ML";
    8.33 -
    8.34 -if ML_System.name = "polyml-5.6"
    8.35 -then use "RAW/exn_trace.ML"
    8.36 -else use "RAW/exn_trace_raw.ML";
    8.37 +use "RAW/exn_trace.ML";
    8.38  
    8.39  
    8.40  (* multithreading *)
    8.41  
    8.42  val seconds = Time.fromReal;
    8.43  
    8.44 -if List.exists (fn s => s = "SingleAssignment") (PolyML.Compiler.structureNames ())
    8.45 -then ()
    8.46 -else use "RAW/single_assignment_polyml.ML";
    8.47 -
    8.48  open Thread;
    8.49  use "RAW/multithreading.ML";
    8.50  
    8.51 -if ML_System.name = "polyml-5.6"
    8.52 -then use "RAW/ml_stack_polyml-5.6.ML"
    8.53 -else use "RAW/ml_stack_dummy.ML";
    8.54 -
    8.55  use "RAW/unsynchronized.ML";
    8.56  val _ = PolyML.Compiler.forgetValue "ref";
    8.57  val _ = PolyML.Compiler.forgetType "ref";
    8.58 @@ -93,9 +72,8 @@
    8.59  
    8.60  (* ML runtime system *)
    8.61  
    8.62 -if ML_System.name = "polyml-5.6"
    8.63 -then use "RAW/ml_profiling_polyml-5.6.ML"
    8.64 -else use "RAW/ml_profiling_polyml.ML";
    8.65 +use "RAW/ml_heap.ML";
    8.66 +use "RAW/ml_profiling.ML";
    8.67  
    8.68  val pointer_eq = PolyML.pointerEq;
    8.69  
    8.70 @@ -162,10 +140,6 @@
    8.71    val display_val = pretty_ml o displayVal;
    8.72  end;
    8.73  
    8.74 -use "RAW/ml_compiler_parameters.ML";
    8.75 -if ML_System.name = "polyml-5.6"
    8.76 -then use "RAW/ml_compiler_parameters_polyml-5.6.ML" else ();
    8.77 -
    8.78  use "RAW/ml_positions.ML";
    8.79  use "RAW/ml_compiler0.ML";
    8.80  
    8.81 @@ -175,10 +149,6 @@
    8.82  PolyML.Compiler.prompt1 := "ML> ";
    8.83  PolyML.Compiler.prompt2 := "ML# ";
    8.84  
    8.85 -use "RAW/ml_parse_tree.ML";
    8.86 -if ML_System.name = "polyml-5.6"
    8.87 -then use "RAW/ml_parse_tree_polyml-5.6.ML" else ();
    8.88 -
    8.89  fun ml_make_string struct_name =
    8.90    "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, FixedInt.fromInt (" ^
    8.91      struct_name ^ ".ML_print_depth ()))))))";
    8.92 @@ -186,6 +156,4 @@
    8.93  
    8.94  (* ML debugger *)
    8.95  
    8.96 -if ML_System.name = "polyml-5.6"
    8.97 -then use_no_debug "RAW/ml_debugger_polyml-5.6.ML"
    8.98 -else use_no_debug "RAW/ml_debugger.ML";
    8.99 +use_no_debug "RAW/ml_debugger.ML";
     9.1 --- a/src/Pure/RAW/exn_trace_raw.ML	Wed Mar 02 19:43:31 2016 +0100
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,8 +0,0 @@
     9.4 -(*  Title:      Pure/RAW/exn_trace_raw.ML
     9.5 -    Author:     Makarius
     9.6 -
     9.7 -Raw exception trace for Poly/ML 5.3.0.
     9.8 -*)
     9.9 -
    9.10 -fun print_exception_trace (_: exn -> string) (_: string -> unit) =
    9.11 -  PolyML.exception_trace;
    10.1 --- a/src/Pure/RAW/ml_compiler0.ML	Wed Mar 02 19:43:31 2016 +0100
    10.2 +++ b/src/Pure/RAW/ml_compiler0.ML	Thu Mar 03 11:12:02 2016 +0100
    10.3 @@ -58,8 +58,8 @@
    10.4        PolyML.Compiler.CPErrorMessageProc put_message,
    10.5        PolyML.Compiler.CPLineNo (fn () => ! current_line),
    10.6        PolyML.Compiler.CPFileName file,
    10.7 -      PolyML.Compiler.CPPrintInAlphabeticalOrder false] @
    10.8 -      ML_Compiler_Parameters.debug debug;
    10.9 +      PolyML.Compiler.CPPrintInAlphabeticalOrder false,
   10.10 +      PolyML.Compiler.CPDebug debug];
   10.11      val _ =
   10.12        (while not (List.null (! in_buffer)) do
   10.13          PolyML.compiler (get, parameters) ())
    11.1 --- a/src/Pure/RAW/ml_compiler_parameters.ML	Wed Mar 02 19:43:31 2016 +0100
    11.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.3 @@ -1,17 +0,0 @@
    11.4 -(*  Title:      Pure/RAW/ml_compiler_parameters.ML
    11.5 -    Author:     Makarius
    11.6 -
    11.7 -Additional ML compiler parameters for Poly/ML.
    11.8 -*)
    11.9 -
   11.10 -signature ML_COMPILER_PARAMETERS =
   11.11 -sig
   11.12 -  val debug: bool -> PolyML.Compiler.compilerParameters list
   11.13 -end;
   11.14 -
   11.15 -structure ML_Compiler_Parameters: ML_COMPILER_PARAMETERS =
   11.16 -struct
   11.17 -
   11.18 -fun debug _ = [];
   11.19 -
   11.20 -end;
   11.21 \ No newline at end of file
    12.1 --- a/src/Pure/RAW/ml_compiler_parameters_polyml-5.6.ML	Wed Mar 02 19:43:31 2016 +0100
    12.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.3 @@ -1,12 +0,0 @@
    12.4 -(*  Title:      Pure/RAW/ml_compiler_parameters_polyml-5.6.ML
    12.5 -    Author:     Makarius
    12.6 -
    12.7 -Additional ML compiler parameters for Poly/ML 5.6, or later.
    12.8 -*)
    12.9 -
   12.10 -structure ML_Compiler_Parameters: ML_COMPILER_PARAMETERS =
   12.11 -struct
   12.12 -
   12.13 -fun debug b = [PolyML.Compiler.CPDebug b];
   12.14 -
   12.15 -end;
   12.16 \ No newline at end of file
    13.1 --- a/src/Pure/RAW/ml_debugger.ML	Wed Mar 02 19:43:31 2016 +0100
    13.2 +++ b/src/Pure/RAW/ml_debugger.ML	Thu Mar 03 11:12:02 2016 +0100
    13.3 @@ -1,7 +1,7 @@
    13.4  (*  Title:      Pure/RAW/ml_debugger.ML
    13.5      Author:     Makarius
    13.6  
    13.7 -ML debugger interface -- dummy version.
    13.8 +ML debugger interface -- for Poly/ML 5.6, or later.
    13.9  *)
   13.10  
   13.11  signature ML_DEBUGGER =
   13.12 @@ -10,16 +10,17 @@
   13.13    val exn_id: exn -> exn_id
   13.14    val print_exn_id: exn_id -> string
   13.15    val eq_exn_id: exn_id * exn_id -> bool
   13.16 -  val on_entry: (string * 'location -> unit) option -> unit
   13.17 -  val on_exit: (string * 'location -> unit) option -> unit
   13.18 -  val on_exit_exception: (string * 'location -> exn -> unit) option -> unit
   13.19 -  val on_breakpoint: ('location * bool Unsynchronized.ref -> unit) option -> unit
   13.20 +  type location
   13.21 +  val on_entry: (string * location -> unit) option -> unit
   13.22 +  val on_exit: (string * location -> unit) option -> unit
   13.23 +  val on_exit_exception: (string * location -> exn -> unit) option -> unit
   13.24 +  val on_breakpoint: (location * bool Unsynchronized.ref -> unit) option -> unit
   13.25    type state
   13.26    val state: Thread.thread -> state list
   13.27    val debug_function: state -> string
   13.28    val debug_function_arg: state -> ML_Name_Space.valueVal
   13.29    val debug_function_result: state -> ML_Name_Space.valueVal
   13.30 -  val debug_location: state -> 'location
   13.31 +  val debug_location: state -> location
   13.32    val debug_name_space: state -> ML_Name_Space.T
   13.33    val debug_local_name_space: state -> ML_Name_Space.T
   13.34  end;
   13.35 @@ -29,36 +30,43 @@
   13.36  
   13.37  (* exceptions *)
   13.38  
   13.39 -abstype exn_id = Exn_Id of string
   13.40 +abstype exn_id = Exn_Id of string * int Unsynchronized.ref
   13.41  with
   13.42  
   13.43 -fun exn_id exn = Exn_Id (General.exnName exn);
   13.44 -fun print_exn_id (Exn_Id name) = name;
   13.45 -fun eq_exn_id (Exn_Id name1, Exn_Id name2) = name1 = name2;  (*over-approximation*)
   13.46 +fun exn_id exn =
   13.47 +  Exn_Id (General.exnName exn, RunCall.run_call2 RuntimeCalls.POLY_SYS_load_word (exn, 0));
   13.48 +
   13.49 +fun print_exn_id (Exn_Id (name, _)) = name;
   13.50 +fun eq_exn_id (Exn_Id (_, id1), Exn_Id (_, id2)) = PolyML.pointerEq (id1, id2);
   13.51  
   13.52  end;
   13.53  
   13.54 +val _ =
   13.55 +  PolyML.addPrettyPrinter (fn _ => fn _ => fn exn_id =>
   13.56 +    let val s = print_exn_id exn_id
   13.57 +    in ml_pretty (ML_Pretty.String (s, FixedInt.fromInt (size s))) end);
   13.58 +
   13.59  
   13.60  (* hooks *)
   13.61  
   13.62 -fun on_entry _ = ();
   13.63 -fun on_exit _ = ();
   13.64 -fun on_exit_exception _ = ();
   13.65 -fun on_breakpoint _ = ();
   13.66 +type location = PolyML.location;
   13.67 +
   13.68 +val on_entry = PolyML.DebuggerInterface.setOnEntry;
   13.69 +val on_exit = PolyML.DebuggerInterface.setOnExit;
   13.70 +val on_exit_exception = PolyML.DebuggerInterface.setOnExitException;
   13.71 +val on_breakpoint = PolyML.DebuggerInterface.setOnBreakPoint;
   13.72  
   13.73  
   13.74 -(* debugger *)
   13.75 +(* debugger operations *)
   13.76  
   13.77 -fun fail () = raise Fail "No debugger support on this ML platform";
   13.78 -
   13.79 -type state = unit;
   13.80 +type state = PolyML.DebuggerInterface.debugState;
   13.81  
   13.82 -fun state _ = [];
   13.83 -fun debug_function () = fail ();
   13.84 -fun debug_function_arg () = fail ();
   13.85 -fun debug_function_result () = fail ();
   13.86 -fun debug_location () = fail ();
   13.87 -fun debug_name_space () = fail ();
   13.88 -fun debug_local_name_space () = fail ();
   13.89 +val state = PolyML.DebuggerInterface.debugState;
   13.90 +val debug_function = PolyML.DebuggerInterface.debugFunction;
   13.91 +val debug_function_arg = PolyML.DebuggerInterface.debugFunctionArg;
   13.92 +val debug_function_result = PolyML.DebuggerInterface.debugFunctionResult;
   13.93 +val debug_location = PolyML.DebuggerInterface.debugLocation;
   13.94 +val debug_name_space = PolyML.DebuggerInterface.debugNameSpace;
   13.95 +val debug_local_name_space = PolyML.DebuggerInterface.debugLocalNameSpace;
   13.96  
   13.97  end;
    14.1 --- a/src/Pure/RAW/ml_debugger_polyml-5.6.ML	Wed Mar 02 19:43:31 2016 +0100
    14.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.3 @@ -1,72 +0,0 @@
    14.4 -(*  Title:      Pure/RAW/ml_debugger_polyml-5.6.ML
    14.5 -    Author:     Makarius
    14.6 -
    14.7 -ML debugger interface -- for Poly/ML 5.6, or later.
    14.8 -*)
    14.9 -
   14.10 -signature ML_DEBUGGER =
   14.11 -sig
   14.12 -  type exn_id
   14.13 -  val exn_id: exn -> exn_id
   14.14 -  val print_exn_id: exn_id -> string
   14.15 -  val eq_exn_id: exn_id * exn_id -> bool
   14.16 -  type location
   14.17 -  val on_entry: (string * location -> unit) option -> unit
   14.18 -  val on_exit: (string * location -> unit) option -> unit
   14.19 -  val on_exit_exception: (string * location -> exn -> unit) option -> unit
   14.20 -  val on_breakpoint: (location * bool Unsynchronized.ref -> unit) option -> unit
   14.21 -  type state
   14.22 -  val state: Thread.thread -> state list
   14.23 -  val debug_function: state -> string
   14.24 -  val debug_function_arg: state -> ML_Name_Space.valueVal
   14.25 -  val debug_function_result: state -> ML_Name_Space.valueVal
   14.26 -  val debug_location: state -> location
   14.27 -  val debug_name_space: state -> ML_Name_Space.T
   14.28 -  val debug_local_name_space: state -> ML_Name_Space.T
   14.29 -end;
   14.30 -
   14.31 -structure ML_Debugger: ML_DEBUGGER =
   14.32 -struct
   14.33 -
   14.34 -(* exceptions *)
   14.35 -
   14.36 -abstype exn_id = Exn_Id of string * int Unsynchronized.ref
   14.37 -with
   14.38 -
   14.39 -fun exn_id exn =
   14.40 -  Exn_Id (General.exnName exn, RunCall.run_call2 RuntimeCalls.POLY_SYS_load_word (exn, 0));
   14.41 -
   14.42 -fun print_exn_id (Exn_Id (name, _)) = name;
   14.43 -fun eq_exn_id (Exn_Id (_, id1), Exn_Id (_, id2)) = PolyML.pointerEq (id1, id2);
   14.44 -
   14.45 -end;
   14.46 -
   14.47 -val _ =
   14.48 -  PolyML.addPrettyPrinter (fn _ => fn _ => fn exn_id =>
   14.49 -    let val s = print_exn_id exn_id
   14.50 -    in ml_pretty (ML_Pretty.String (s, FixedInt.fromInt (size s))) end);
   14.51 -
   14.52 -
   14.53 -(* hooks *)
   14.54 -
   14.55 -type location = PolyML.location;
   14.56 -
   14.57 -val on_entry = PolyML.DebuggerInterface.setOnEntry;
   14.58 -val on_exit = PolyML.DebuggerInterface.setOnExit;
   14.59 -val on_exit_exception = PolyML.DebuggerInterface.setOnExitException;
   14.60 -val on_breakpoint = PolyML.DebuggerInterface.setOnBreakPoint;
   14.61 -
   14.62 -
   14.63 -(* debugger operations *)
   14.64 -
   14.65 -type state = PolyML.DebuggerInterface.debugState;
   14.66 -
   14.67 -val state = PolyML.DebuggerInterface.debugState;
   14.68 -val debug_function = PolyML.DebuggerInterface.debugFunction;
   14.69 -val debug_function_arg = PolyML.DebuggerInterface.debugFunctionArg;
   14.70 -val debug_function_result = PolyML.DebuggerInterface.debugFunctionResult;
   14.71 -val debug_location = PolyML.DebuggerInterface.debugLocation;
   14.72 -val debug_name_space = PolyML.DebuggerInterface.debugNameSpace;
   14.73 -val debug_local_name_space = PolyML.DebuggerInterface.debugLocalNameSpace;
   14.74 -
   14.75 -end;
    15.1 --- a/src/Pure/RAW/ml_heap_polyml-5.3.0.ML	Wed Mar 02 19:43:31 2016 +0100
    15.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.3 @@ -1,17 +0,0 @@
    15.4 -(*  Title:      Pure/RAW/ml_heap_polyml-5.3.0.ML
    15.5 -    Author:     Makarius
    15.6 -
    15.7 -ML heap operations.
    15.8 -*)
    15.9 -
   15.10 -signature ML_HEAP =
   15.11 -sig
   15.12 -  val share_common_data: unit -> unit
   15.13 -  val save_state: string -> unit
   15.14 -end;
   15.15 -
   15.16 -structure ML_Heap: ML_HEAP =
   15.17 -struct
   15.18 -  fun share_common_data () = ();
   15.19 -  val save_state = PolyML.SaveState.saveState o ML_System.platform_path;
   15.20 -end;
    16.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.2 +++ b/src/Pure/RAW/ml_name_space.ML	Thu Mar 03 11:12:02 2016 +0100
    16.3 @@ -0,0 +1,33 @@
    16.4 +(*  Title:      Pure/RAW/ml_name_space.ML
    16.5 +    Author:     Makarius
    16.6 +
    16.7 +Name space for Poly/ML.
    16.8 +*)
    16.9 +
   16.10 +structure ML_Name_Space =
   16.11 +struct
   16.12 +  open PolyML.NameSpace;
   16.13 +
   16.14 +  type T = PolyML.NameSpace.nameSpace;
   16.15 +  val global = PolyML.globalNameSpace;
   16.16 +  val forget_global_structure = PolyML.Compiler.forgetStructure;
   16.17 +
   16.18 +  type valueVal = Values.value;
   16.19 +  fun displayVal (x, depth, space) = Values.printWithType (x, depth, SOME space);
   16.20 +  fun displayTypeExpression (x, depth, space) = Values.printType (x, depth, SOME space);
   16.21 +
   16.22 +  type typeVal = TypeConstrs.typeConstr;
   16.23 +  fun displayType (x, depth, space) = TypeConstrs.print (x, depth, SOME space);
   16.24 +
   16.25 +  type fixityVal = Infixes.fixity;
   16.26 +  fun displayFix (_: string, x) = Infixes.print x;
   16.27 +
   16.28 +  type structureVal = Structures.structureVal;
   16.29 +  fun displayStruct (x, depth, space) = Structures.print (x, depth, SOME space);
   16.30 +
   16.31 +  type signatureVal = Signatures.signatureVal;
   16.32 +  fun displaySig (x, depth, space) = Signatures.print (x, depth, SOME space);
   16.33 +
   16.34 +  type functorVal = Functors.functorVal;
   16.35 +  fun displayFunct (x, depth, space) = Functors.print (x, depth, SOME space);
   16.36 +end;
    17.1 --- a/src/Pure/RAW/ml_name_space_polyml-5.6.ML	Wed Mar 02 19:43:31 2016 +0100
    17.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.3 @@ -1,33 +0,0 @@
    17.4 -(*  Title:      Pure/RAW/ml_name_space_polyml-5.6.ML
    17.5 -    Author:     Makarius
    17.6 -
    17.7 -Name space for Poly/ML.
    17.8 -*)
    17.9 -
   17.10 -structure ML_Name_Space =
   17.11 -struct
   17.12 -  open PolyML.NameSpace;
   17.13 -
   17.14 -  type T = PolyML.NameSpace.nameSpace;
   17.15 -  val global = PolyML.globalNameSpace;
   17.16 -  val forget_global_structure = PolyML.Compiler.forgetStructure;
   17.17 -
   17.18 -  type valueVal = Values.value;
   17.19 -  fun displayVal (x, depth, space) = Values.printWithType (x, depth, SOME space);
   17.20 -  fun displayTypeExpression (x, depth, space) = Values.printType (x, depth, SOME space);
   17.21 -
   17.22 -  type typeVal = TypeConstrs.typeConstr;
   17.23 -  fun displayType (x, depth, space) = TypeConstrs.print (x, depth, SOME space);
   17.24 -
   17.25 -  type fixityVal = Infixes.fixity;
   17.26 -  fun displayFix (_: string, x) = Infixes.print x;
   17.27 -
   17.28 -  type structureVal = Structures.structureVal;
   17.29 -  fun displayStruct (x, depth, space) = Structures.print (x, depth, SOME space);
   17.30 -
   17.31 -  type signatureVal = Signatures.signatureVal;
   17.32 -  fun displaySig (x, depth, space) = Signatures.print (x, depth, SOME space);
   17.33 -
   17.34 -  type functorVal = Functors.functorVal;
   17.35 -  fun displayFunct (x, depth, space) = Functors.print (x, depth, SOME space);
   17.36 -end;
    18.1 --- a/src/Pure/RAW/ml_name_space_polyml.ML	Wed Mar 02 19:43:31 2016 +0100
    18.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    18.3 @@ -1,13 +0,0 @@
    18.4 -(*  Title:      Pure/RAW/ml_name_space_polyml.ML
    18.5 -    Author:     Makarius
    18.6 -
    18.7 -Name space for Poly/ML.
    18.8 -*)
    18.9 -
   18.10 -structure ML_Name_Space =
   18.11 -struct
   18.12 -  open PolyML.NameSpace;
   18.13 -  type T = nameSpace;
   18.14 -  val global = PolyML.globalNameSpace;
   18.15 -  val forget_global_structure = PolyML.Compiler.forgetStructure;
   18.16 -end;
    19.1 --- a/src/Pure/RAW/ml_parse_tree.ML	Wed Mar 02 19:43:31 2016 +0100
    19.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    19.3 @@ -1,19 +0,0 @@
    19.4 -(*  Title:      Pure/RAW/ml_parse_tree.ML
    19.5 -    Author:     Makarius
    19.6 -
    19.7 -Additional ML parse tree components for Poly/ML.
    19.8 -*)
    19.9 -
   19.10 -signature ML_PARSE_TREE =
   19.11 -sig
   19.12 -  val completions: PolyML.ptProperties -> string list option
   19.13 -  val breakpoint: PolyML.ptProperties -> bool Unsynchronized.ref option
   19.14 -end;
   19.15 -
   19.16 -structure ML_Parse_Tree: ML_PARSE_TREE =
   19.17 -struct
   19.18 -
   19.19 -fun completions _ = NONE;
   19.20 -fun breakpoint _ = NONE;
   19.21 -
   19.22 -end;
   19.23 \ No newline at end of file
    20.1 --- a/src/Pure/RAW/ml_parse_tree_polyml-5.6.ML	Wed Mar 02 19:43:31 2016 +0100
    20.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    20.3 @@ -1,16 +0,0 @@
    20.4 -(*  Title:      Pure/RAW/ml_parse_tree_polyml-5.6.ML
    20.5 -    Author:     Makarius
    20.6 -
    20.7 -Additional ML parse tree components for Poly/ML 5.6, or later.
    20.8 -*)
    20.9 -
   20.10 -structure ML_Parse_Tree: ML_PARSE_TREE =
   20.11 -struct
   20.12 -
   20.13 -fun completions (PolyML.PTcompletions x) = SOME x
   20.14 -  | completions _ = NONE;
   20.15 -
   20.16 -fun breakpoint (PolyML.PTbreakPoint x) = SOME x
   20.17 -  | breakpoint _ = NONE;
   20.18 -
   20.19 -end;
   20.20 \ No newline at end of file
    21.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    21.2 +++ b/src/Pure/RAW/ml_profiling.ML	Thu Mar 03 11:12:02 2016 +0100
    21.3 @@ -0,0 +1,19 @@
    21.4 +(*  Title:      Pure/RAW/ml_profiling.ML
    21.5 +    Author:     Makarius
    21.6 +
    21.7 +Profiling for Poly/ML 5.6.
    21.8 +*)
    21.9 +
   21.10 +structure ML_Profiling =
   21.11 +struct
   21.12 +
   21.13 +fun profile_time pr f x =
   21.14 +  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTime f x;
   21.15 +
   21.16 +fun profile_time_thread pr f x =
   21.17 +  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTimeThisThread f x;
   21.18 +
   21.19 +fun profile_allocations pr f x =
   21.20 +  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileAllocations f x;
   21.21 +
   21.22 +end;
    22.1 --- a/src/Pure/RAW/ml_profiling_polyml-5.6.ML	Wed Mar 02 19:43:31 2016 +0100
    22.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    22.3 @@ -1,19 +0,0 @@
    22.4 -(*  Title:      Pure/RAW/ml_profiling_polyml-5.6.ML
    22.5 -    Author:     Makarius
    22.6 -
    22.7 -Profiling for Poly/ML 5.6.
    22.8 -*)
    22.9 -
   22.10 -structure ML_Profiling =
   22.11 -struct
   22.12 -
   22.13 -fun profile_time pr f x =
   22.14 -  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTime f x;
   22.15 -
   22.16 -fun profile_time_thread pr f x =
   22.17 -  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTimeThisThread f x;
   22.18 -
   22.19 -fun profile_allocations pr f x =
   22.20 -  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileAllocations f x;
   22.21 -
   22.22 -end;
    23.1 --- a/src/Pure/RAW/ml_profiling_polyml.ML	Wed Mar 02 19:43:31 2016 +0100
    23.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    23.3 @@ -1,27 +0,0 @@
    23.4 -(*  Title:      Pure/RAW/ml_profiling_polyml.ML
    23.5 -    Author:     Makarius
    23.6 -
    23.7 -Profiling for Poly/ML.
    23.8 -*)
    23.9 -
   23.10 -structure ML_Profiling =
   23.11 -struct
   23.12 -
   23.13 -local
   23.14 -
   23.15 -fun profile n f x =
   23.16 -  let
   23.17 -    val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler n;
   23.18 -    val res = Exn.capture f x;
   23.19 -    val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0;
   23.20 -  in Exn.release res end;
   23.21 -
   23.22 -in
   23.23 -
   23.24 -fun profile_time (_: (int * string) list -> unit) f x = profile 1 f x;
   23.25 -fun profile_time_thread (_: (int * string) list -> unit) f x = profile 6 f x;
   23.26 -fun profile_allocations (_: (int * string) list -> unit) f x = profile 2 f x;
   23.27 -
   23.28 -end;
   23.29 -
   23.30 -end;
    24.1 --- a/src/Pure/RAW/ml_stack_dummy.ML	Wed Mar 02 19:43:31 2016 +0100
    24.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    24.3 @@ -1,16 +0,0 @@
    24.4 -(*  Title:      Pure/RAW/ml_stack_dummy.ML
    24.5 -
    24.6 -Maximum stack size (in words) for ML threads -- dummy version.
    24.7 -*)
    24.8 -
    24.9 -signature ML_STACK =
   24.10 -sig
   24.11 -  val limit: int option -> Thread.threadAttribute list
   24.12 -end;
   24.13 -
   24.14 -structure ML_Stack: ML_STACK =
   24.15 -struct
   24.16 -
   24.17 -fun limit (_: int option) : Thread.threadAttribute list = [];
   24.18 -
   24.19 -end;
    25.1 --- a/src/Pure/RAW/ml_stack_polyml-5.6.ML	Wed Mar 02 19:43:31 2016 +0100
    25.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    25.3 @@ -1,16 +0,0 @@
    25.4 -(*  Title:      Pure/RAW/ml_stack_polyml-5.6.ML
    25.5 -
    25.6 -Maximum stack size (in words) for ML threads -- Poly/ML 5.6, or later.
    25.7 -*)
    25.8 -
    25.9 -signature ML_STACK =
   25.10 -sig
   25.11 -  val limit: int option -> Thread.threadAttribute list
   25.12 -end;
   25.13 -
   25.14 -structure ML_Stack: ML_STACK =
   25.15 -struct
   25.16 -
   25.17 -fun limit m = [Thread.MaximumMLStack m];
   25.18 -
   25.19 -end;
    26.1 --- a/src/Pure/RAW/multithreading.ML	Wed Mar 02 19:43:31 2016 +0100
    26.2 +++ b/src/Pure/RAW/multithreading.ML	Thu Mar 03 11:12:02 2016 +0100
    26.3 @@ -88,8 +88,13 @@
    26.4  
    26.5  (* options *)
    26.6  
    26.7 +fun num_processors () =
    26.8 +  (case Thread.numPhysicalProcessors () of
    26.9 +    SOME n => n
   26.10 +  | NONE => Thread.numProcessors ());
   26.11 +
   26.12  fun max_threads_result m =
   26.13 -  if m > 0 then m else Int.min (Int.max (Thread.numProcessors (), 1), 8);
   26.14 +  if m > 0 then m else Int.min (Int.max (num_processors (), 1), 8);
   26.15  
   26.16  val max_threads = ref 1;
   26.17  
    27.1 --- a/src/Pure/RAW/single_assignment_polyml.ML	Wed Mar 02 19:43:31 2016 +0100
    27.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    27.3 @@ -1,35 +0,0 @@
    27.4 -(*  Title:      Pure/RAW/single_assignment_polyml.ML
    27.5 -    Author:     Makarius
    27.6 -
    27.7 -References with single assignment.  Unsynchronized!  Emulates
    27.8 -structure SingleAssignment from Poly/ML 5.4.
    27.9 -*)
   27.10 -
   27.11 -signature SINGLE_ASSIGNMENT =
   27.12 -sig
   27.13 -  type 'a saref
   27.14 -  exception Locked
   27.15 -  val saref: unit -> 'a saref
   27.16 -  val savalue: 'a saref -> 'a option
   27.17 -  val saset: 'a saref * 'a -> unit
   27.18 -end;
   27.19 -
   27.20 -structure SingleAssignment: SINGLE_ASSIGNMENT =
   27.21 -struct
   27.22 -
   27.23 -exception Locked;
   27.24 -
   27.25 -abstype 'a saref = SARef of 'a option ref
   27.26 -with
   27.27 -
   27.28 -fun saref () = SARef (ref NONE);
   27.29 -
   27.30 -fun savalue (SARef r) = ! r;
   27.31 -
   27.32 -fun saset (SARef (r as ref NONE), x) =
   27.33 -      (r := SOME x; RunCall.run_call1 RuntimeCalls.POLY_SYS_lockseg r)
   27.34 -  | saset _ = raise Locked;
   27.35 -
   27.36 -end;
   27.37 -
   27.38 -end;
    28.1 --- a/src/Pure/ROOT	Wed Mar 02 19:43:31 2016 +0100
    28.2 +++ b/src/Pure/ROOT	Thu Mar 03 11:12:02 2016 +0100
    28.3 @@ -3,65 +3,39 @@
    28.4  session RAW =
    28.5    theories
    28.6    files
    28.7 -    "RAW/ROOT_polyml-5.6.ML"
    28.8      "RAW/ROOT_polyml.ML"
    28.9      "RAW/exn.ML"
   28.10      "RAW/exn_trace.ML"
   28.11 -    "RAW/exn_trace_raw.ML"
   28.12      "RAW/fixed_int_dummy.ML"
   28.13      "RAW/ml_compiler0.ML"
   28.14 -    "RAW/ml_compiler_parameters.ML"
   28.15 -    "RAW/ml_compiler_parameters_polyml-5.6.ML"
   28.16      "RAW/ml_debugger.ML"
   28.17 -    "RAW/ml_debugger_polyml-5.6.ML"
   28.18      "RAW/ml_heap.ML"
   28.19 -    "RAW/ml_heap_polyml-5.3.0.ML"
   28.20 -    "RAW/ml_name_space_polyml-5.6.ML"
   28.21 -    "RAW/ml_name_space_polyml.ML"
   28.22 -    "RAW/ml_parse_tree.ML"
   28.23 -    "RAW/ml_parse_tree_polyml-5.6.ML"
   28.24 +    "RAW/ml_name_space.ML"
   28.25      "RAW/ml_positions.ML"
   28.26      "RAW/ml_pretty.ML"
   28.27 -    "RAW/ml_profiling_polyml-5.6.ML"
   28.28 -    "RAW/ml_profiling_polyml.ML"
   28.29 -    "RAW/ml_stack_dummy.ML"
   28.30 -    "RAW/ml_stack_polyml-5.6.ML"
   28.31 +    "RAW/ml_profiling.ML"
   28.32      "RAW/ml_system.ML"
   28.33      "RAW/multithreading.ML"
   28.34      "RAW/secure.ML"
   28.35 -    "RAW/single_assignment_polyml.ML"
   28.36      "RAW/unsynchronized.ML"
   28.37  
   28.38  session Pure =
   28.39    global_theories Pure
   28.40    files
   28.41 -    "RAW/ROOT_polyml-5.6.ML"
   28.42      "RAW/ROOT_polyml.ML"
   28.43      "RAW/exn.ML"
   28.44      "RAW/exn_trace.ML"
   28.45 -    "RAW/exn_trace_raw.ML"
   28.46      "RAW/fixed_int_dummy.ML"
   28.47      "RAW/ml_compiler0.ML"
   28.48 -    "RAW/ml_compiler_parameters.ML"
   28.49 -    "RAW/ml_compiler_parameters_polyml-5.6.ML"
   28.50      "RAW/ml_debugger.ML"
   28.51 -    "RAW/ml_debugger_polyml-5.6.ML"
   28.52      "RAW/ml_heap.ML"
   28.53 -    "RAW/ml_heap_polyml-5.3.0.ML"
   28.54 -    "RAW/ml_name_space_polyml-5.6.ML"
   28.55 -    "RAW/ml_name_space_polyml.ML"
   28.56 -    "RAW/ml_parse_tree.ML"
   28.57 -    "RAW/ml_parse_tree_polyml-5.6.ML"
   28.58 +    "RAW/ml_name_space.ML"
   28.59      "RAW/ml_positions.ML"
   28.60      "RAW/ml_pretty.ML"
   28.61 -    "RAW/ml_profiling_polyml-5.6.ML"
   28.62 -    "RAW/ml_profiling_polyml.ML"
   28.63 -    "RAW/ml_stack_dummy.ML"
   28.64 -    "RAW/ml_stack_polyml-5.6.ML"
   28.65 +    "RAW/ml_profiling.ML"
   28.66      "RAW/ml_system.ML"
   28.67      "RAW/multithreading.ML"
   28.68      "RAW/secure.ML"
   28.69 -    "RAW/single_assignment_polyml.ML"
   28.70      "RAW/unsynchronized.ML"
   28.71  
   28.72      "Concurrent/bash.ML"
    29.1 --- a/src/Pure/ROOT.ML	Wed Mar 02 19:43:31 2016 +0100
    29.2 +++ b/src/Pure/ROOT.ML	Thu Mar 03 11:12:02 2016 +0100
    29.3 @@ -101,9 +101,7 @@
    29.4  
    29.5  use "ML/exn_properties.ML";
    29.6  
    29.7 -if ML_System.name = "polyml-5.6"
    29.8 -then use "ML/ml_statistics.ML"
    29.9 -else use "ML/ml_statistics_dummy.ML";
   29.10 +use "ML/ml_statistics.ML";
   29.11  
   29.12  use "Concurrent/standard_thread.ML";
   29.13  use "Concurrent/single_assignment.ML";
    30.1 --- a/src/Pure/System/system_channel.ML	Wed Mar 02 19:43:31 2016 +0100
    30.2 +++ b/src/Pure/System/system_channel.ML	Thu Mar 03 11:12:02 2016 +0100
    30.3 @@ -32,8 +32,7 @@
    30.4    in read [] end;
    30.5  
    30.6  fun inputN (System_Channel (in_stream, _)) n =
    30.7 -  if n = 0 then ""  (*workaround for polyml-5.5.1 or earlier*)
    30.8 -  else Byte.bytesToString (BinIO.inputN (in_stream, n));
    30.9 +  Byte.bytesToString (BinIO.inputN (in_stream, n));
   30.10  
   30.11  fun output (System_Channel (_, out_stream)) s =
   30.12    File.output out_stream s;