# HG changeset patch # User wenzelm # Date 1223060798 -7200 # Node ID 40c3f900c4572e3159da81624e6ae1bae48128f3 # Parent 404649964f09018ce9c4a0523e1a5cd450832640 removed obsolete Posix/Signal compatibility wrappers; diff -r 404649964f09 -r 40c3f900c457 src/Pure/ML-Systems/polyml_old_basis.ML --- a/src/Pure/ML-Systems/polyml_old_basis.ML Fri Oct 03 21:06:37 2008 +0200 +++ b/src/Pure/ML-Systems/polyml_old_basis.ML Fri Oct 03 21:06:38 2008 +0200 @@ -21,17 +21,6 @@ val full = all; end; -structure Posix = -struct - open Posix; - structure IO = - struct - open IO; - val mkTextReader = mkReader; - val mkTextWriter = mkWriter; - end; -end; - structure TextIO = struct open TextIO; diff -r 404649964f09 -r 40c3f900c457 src/Pure/ML-Systems/proper_int.ML --- a/src/Pure/ML-Systems/proper_int.ML Fri Oct 03 21:06:37 2008 +0200 +++ b/src/Pure/ML-Systems/proper_int.ML Fri Oct 03 21:06:38 2008 +0200 @@ -193,18 +193,3 @@ fun fmt a b = Time.fmt (dest_int a) b; end; - -(* Posix *) - -structure Posix = -struct - open Posix; - structure IO = - struct - open IO; - fun mkTextWriter {appendMode, chunkSize, fd, initBlkMode, name} = - IO.mkTextWriter {appendMode = appendMode, chunkSize = dest_int chunkSize, - fd = fd, initBlkMode = initBlkMode, name = name}; - end; -end; -