discontinued polyml-5.3.0;

--HG--
rename : src/Pure/RAW/ml_debugger_polyml-5.6.ML => src/Pure/RAW/ml_debugger.ML
rename : src/Pure/RAW/ml_name_space_polyml-5.6.ML => src/Pure/RAW/ml_name_space.ML
rename : src/Pure/RAW/ml_profiling_polyml-5.6.ML => src/Pure/RAW/ml_profiling.ML

precise BinIO, without newline conversion on Windows;

discontinued fifo channel, always use portable socket;

clarified workaround: problem is potential blocking of vacuous input (see also Poly/ML SVN 1874);

avoid empty input and its adverse effect on socket communication, e.g. output message getting "stuck" after vacuous update due to Session.update_options;

recovered buffered sockets from 11f622794ad6 -- requires Poly/ML 5.5.x;

always use sockets on Windows/Cygwin;
discontinued special raw_dump facility;

raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;

abstract System_Channel in ML (cf. Scala version);
back to TextIO for fifo, which is more stable in Poly/ML 5.4.x;
explicit block buffering -- BinIO might be subject to old Poly/ML defaults;