equal
deleted
inserted
replaced
13 struct |
13 struct |
14 fun substring args = String.substring args |
14 fun substring args = String.substring args |
15 handle String.Substring => raise Subscript; |
15 handle String.Substring => raise Subscript; |
16 fun isPrefix s1 s2 = (s1 = substring(s2,0, size s1)) |
16 fun isPrefix s1 s2 = (s1 = substring(s2,0, size s1)) |
17 handle Subscript => false; |
17 handle Subscript => false; |
|
18 fun str (s : string) = s; |
|
19 fun translate f s = implode (map f (explode s)); |
18 end; |
20 end; |
19 |
21 |
20 |
22 |
21 |
23 |
22 (** ML system related **) |
24 (** ML system related **) |