src/Pure/ML-Systems/polyml-old-basis.ML
changeset 23139 aa899bce7c3b
child 23141 1f6b6a7314cf
equal deleted inserted replaced
23138:6852373aae8a 23139:aa899bce7c3b
       
     1 (*  Title:      Pure/ML-Systems/polyml-old-basis.ML
       
     2     ID:         $Id$
       
     3 
       
     4 Fixes for the old SML basis library (before Poly/ML 4.2.0).
       
     5 *)
       
     6 
       
     7 structure String =
       
     8 struct
       
     9   open String;
       
    10   fun isSuffix s1 s2 =
       
    11     let val n1 = size s1 and n2 = size s2
       
    12     in if n1 = n2 then s1 = s2 else n1 <= n2 andalso String.substring (s2, n2 - n1, n1) = s1 end;
       
    13 end;
       
    14 
       
    15 structure Substring =
       
    16 struct
       
    17   open Substring;
       
    18   val full = all;
       
    19 end;
       
    20 
       
    21 structure Posix =
       
    22 struct
       
    23   open Posix;
       
    24   structure IO =
       
    25   struct
       
    26     open IO;
       
    27     val mkTextReader = mkReader;
       
    28     val mkTextWriter = mkWriter;
       
    29   end;
       
    30 end;