src/Pure/ML-Systems/polyml-old-basis.ML
author berghofe
Mon Jan 21 14:18:49 2008 +0100 (2008-01-21)
changeset 25939 ddea202704b4
parent 24564 260a65fa2900
permissions -rw-r--r--
Removed Logic.auto_rename.
     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;