| author | wenzelm |
| Fri, 03 Oct 2008 21:06:38 +0200 | |
| changeset 28490 | 40c3f900c457 |
| parent 26216 | c7d0cd2c7715 |
| child 29564 | f8b933a62151 |
| permissions | -rw-r--r-- |
1 (* Title: Pure/ML-Systems/polyml_old_basis.ML
2 ID: $Id$
4 Fixes for the old SML basis library (before Poly/ML 4.2.0).
5 *)
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;
18 structure Substring =
19 struct
20 open Substring;
21 val full = all;
22 end;
24 structure TextIO =
25 struct
26 open TextIO;
27 fun inputLine is =
28 let val s = TextIO.inputLine is
29 in if s = "" then NONE else SOME s end;
30 end;