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;
wenzelm@26216
     1
(*  Title:      Pure/ML-Systems/polyml_old_basis.ML
wenzelm@26216
     2
    ID:         $Id$
wenzelm@26216
     3
wenzelm@26216
     4
Fixes for the old SML basis library (before Poly/ML 4.2.0).
wenzelm@26216
     5
*)
wenzelm@26216
     6
wenzelm@26216
     7
structure String =
wenzelm@26216
     8
struct
wenzelm@26216
     9
  fun isSuffix s1 s2 =
wenzelm@26216
    10
    let val n1 = size s1 and n2 = size s2
wenzelm@26216
    11
    in if n1 = n2 then s1 = s2 else n1 <= n2 andalso String.substring (s2, n2 - n1, n1) = s1 end;
wenzelm@26216
    12
  fun isSubstring s1 s2 =
wenzelm@26216
    13
    String.isPrefix s1 s2 orelse
wenzelm@26216
    14
      size s1 < size s2 andalso isSubstring s1 (String.extract (s2, 1, NONE)); 
wenzelm@26216
    15
  open String;
wenzelm@26216
    16
end;
wenzelm@26216
    17
wenzelm@26216
    18
structure Substring =
wenzelm@26216
    19
struct
wenzelm@26216
    20
  open Substring;
wenzelm@26216
    21
  val full = all;
wenzelm@26216
    22
end;
wenzelm@26216
    23
wenzelm@26216
    24
structure Posix =
wenzelm@26216
    25
struct
wenzelm@26216
    26
  open Posix;
wenzelm@26216
    27
  structure IO =
wenzelm@26216
    28
  struct
wenzelm@26216
    29
    open IO;
wenzelm@26216
    30
    val mkTextReader = mkReader;
wenzelm@26216
    31
    val mkTextWriter = mkWriter;
wenzelm@26216
    32
  end;
wenzelm@26216
    33
end;
wenzelm@26216
    34
wenzelm@26216
    35
structure TextIO =
wenzelm@26216
    36
struct
wenzelm@26216
    37
  open TextIO;
wenzelm@26216
    38
  fun inputLine is =
wenzelm@26216
    39
    let val s = TextIO.inputLine is
wenzelm@26216
    40
    in if s = "" then NONE else SOME s end;
wenzelm@26216
    41
end;