src/Pure/ML-Systems/polyml_old_basis.ML
author wenzelm
Sun Mar 01 23:36:12 2009 +0100 (2009-03-01)
changeset 30190 479806475f3c
parent 29564 f8b933a62151
permissions -rw-r--r--
use long names for old-style fold combinators;
wenzelm@26216
     1
(*  Title:      Pure/ML-Systems/polyml_old_basis.ML
wenzelm@26216
     2
wenzelm@26216
     3
Fixes for the old SML basis library (before Poly/ML 4.2.0).
wenzelm@26216
     4
*)
wenzelm@26216
     5
wenzelm@26216
     6
structure String =
wenzelm@26216
     7
struct
wenzelm@26216
     8
  fun isSuffix s1 s2 =
wenzelm@26216
     9
    let val n1 = size s1 and n2 = size s2
wenzelm@26216
    10
    in if n1 = n2 then s1 = s2 else n1 <= n2 andalso String.substring (s2, n2 - n1, n1) = s1 end;
wenzelm@26216
    11
  fun isSubstring s1 s2 =
wenzelm@26216
    12
    String.isPrefix s1 s2 orelse
wenzelm@26216
    13
      size s1 < size s2 andalso isSubstring s1 (String.extract (s2, 1, NONE)); 
wenzelm@26216
    14
  open String;
wenzelm@26216
    15
end;
wenzelm@26216
    16
wenzelm@26216
    17
structure Substring =
wenzelm@26216
    18
struct
wenzelm@26216
    19
  open Substring;
wenzelm@26216
    20
  val full = all;
wenzelm@26216
    21
end;
wenzelm@26216
    22
wenzelm@26216
    23
structure TextIO =
wenzelm@26216
    24
struct
wenzelm@26216
    25
  open TextIO;
wenzelm@26216
    26
  fun inputLine is =
wenzelm@26216
    27
    let val s = TextIO.inputLine is
wenzelm@26216
    28
    in if s = "" then NONE else SOME s end;
wenzelm@26216
    29
end;