equal
deleted
inserted
replaced
|
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 open String; |
|
10 fun isSuffix s1 s2 = |
|
11 let val n1 = size s1 and n2 = size s2 |
|
12 in if n1 = n2 then s1 = s2 else n1 <= n2 andalso String.substring (s2, n2 - n1, n1) = s1 end; |
|
13 end; |
|
14 |
|
15 structure Substring = |
|
16 struct |
|
17 open Substring; |
|
18 val full = all; |
|
19 end; |
|
20 |
|
21 structure Posix = |
|
22 struct |
|
23 open Posix; |
|
24 structure IO = |
|
25 struct |
|
26 open IO; |
|
27 val mkTextReader = mkReader; |
|
28 val mkTextWriter = mkWriter; |
|
29 end; |
|
30 end; |