equal
deleted
inserted
replaced
14 |
14 |
15 structure String = |
15 structure String = |
16 struct |
16 struct |
17 fun substring (s,i,j) = StringBuiltIns.substring (s, i+1, j) |
17 fun substring (s,i,j) = StringBuiltIns.substring (s, i+1, j) |
18 handle Substring => raise Subscript |
18 handle Substring => raise Subscript |
|
19 fun isPrefix s1 s2 = (s1 = substring(s2,0, size s1)) |
|
20 handle Subscript => false |
19 val concat = implode |
21 val concat = implode |
20 end; |
22 end; |
21 |
23 |
22 |
24 |
23 (** ML system related **) |
25 (** ML system related **) |