src/Pure/ML-Systems/polyml_old_basis.ML
changeset 26216 c7d0cd2c7715
child 28490 40c3f900c457
equal deleted inserted replaced
26215:94d32a7cd0fb 26216:c7d0cd2c7715
       
     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   fun isSuffix s1 s2 =
       
    10     let val n1 = size s1 and n2 = size s2
       
    11     in if n1 = n2 then s1 = s2 else n1 <= n2 andalso String.substring (s2, n2 - n1, n1) = s1 end;
       
    12   fun isSubstring s1 s2 =
       
    13     String.isPrefix s1 s2 orelse
       
    14       size s1 < size s2 andalso isSubstring s1 (String.extract (s2, 1, NONE)); 
       
    15   open String;
       
    16 end;
       
    17 
       
    18 structure Substring =
       
    19 struct
       
    20   open Substring;
       
    21   val full = all;
       
    22 end;
       
    23 
       
    24 structure Posix =
       
    25 struct
       
    26   open Posix;
       
    27   structure IO =
       
    28   struct
       
    29     open IO;
       
    30     val mkTextReader = mkReader;
       
    31     val mkTextWriter = mkWriter;
       
    32   end;
       
    33 end;
       
    34 
       
    35 structure TextIO =
       
    36 struct
       
    37   open TextIO;
       
    38   fun inputLine is =
       
    39     let val s = TextIO.inputLine is
       
    40     in if s = "" then NONE else SOME s end;
       
    41 end;