23139
|
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;
|
24564
|
12 |
fun isSubstring s1 s2 =
|
|
13 |
String.isPrefix s1 s2 orelse
|
|
14 |
size s1 < size s2 andalso isSubstring s1 (String.extract (s2, 1, NONE));
|
23141
|
15 |
open String;
|
23139
|
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;
|
23141
|
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;
|