src/Pure/ML-Systems/polyml-old-basis.ML
changeset 23141 1f6b6a7314cf
parent 23139 aa899bce7c3b
child 24564 260a65fa2900
equal deleted inserted replaced
23140:f6927a08a02b 23141:1f6b6a7314cf
     4 Fixes for the old SML basis library (before Poly/ML 4.2.0).
     4 Fixes for the old SML basis library (before Poly/ML 4.2.0).
     5 *)
     5 *)
     6 
     6 
     7 structure String =
     7 structure String =
     8 struct
     8 struct
     9   open String;
       
    10   fun isSuffix s1 s2 =
     9   fun isSuffix s1 s2 =
    11     let val n1 = size s1 and n2 = size s2
    10     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;
    11     in if n1 = n2 then s1 = s2 else n1 <= n2 andalso String.substring (s2, n2 - n1, n1) = s1 end;
       
    12   open String;
    13 end;
    13 end;
    14 
    14 
    15 structure Substring =
    15 structure Substring =
    16 struct
    16 struct
    17   open Substring;
    17   open Substring;
    26     open IO;
    26     open IO;
    27     val mkTextReader = mkReader;
    27     val mkTextReader = mkReader;
    28     val mkTextWriter = mkWriter;
    28     val mkTextWriter = mkWriter;
    29   end;
    29   end;
    30 end;
    30 end;
       
    31 
       
    32 structure TextIO =
       
    33 struct
       
    34   open TextIO;
       
    35   fun inputLine is =
       
    36     let val s = TextIO.inputLine is
       
    37     in if s = "" then NONE else SOME s end;
       
    38 end;