author | wenzelm |
Sun, 10 Dec 2006 15:30:40 +0100 | |
changeset 21742 | a330e58226d0 |
parent 21299 | 4b01726d71fc |
permissions | -rw-r--r-- |
(* Title: Pure/ML-Systems/polyml-4.1.4-patch.ML ID: $Id$ Basis library fixes for Poly/ML 4.2.0 or later. *) structure Posix = struct open Posix; structure IO = struct open IO; val mkReader = mkTextReader; val mkWriter = mkTextWriter; end; end; structure TextIO = struct open TextIO; fun inputLine is = Option.getOpt (TextIO.inputLine is, ""); end; structure Substring = struct open Substring; val all = full; end;