src/Pure/ML-Systems/polyml_old_basis.ML
author wenzelm
Thu Sep 04 16:03:47 2008 +0200 (2008-09-04)
changeset 28124 10a1f1f4c6ae
parent 26216 c7d0cd2c7715
child 28490 40c3f900c457
permissions -rw-r--r--
moved Multithreading.task/schedule to Concurrent/schedule.ML;
     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;