author | wenzelm |
Thu, 10 May 2007 00:39:54 +0200 | |
changeset 22908 | ed66fbbe4a62 |
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;