provide String structure;
authorwenzelm
Mon, 02 Aug 1999 15:39:23 +0200
changeset 7149d0c2168f7704
parent 7148 e9c253036b45
child 7150 d203e2282789
provide String structure;
src/Pure/ML-Systems/smlnj-0.93.ML
     1.1 --- a/src/Pure/ML-Systems/smlnj-0.93.ML	Mon Aug 02 15:39:04 1999 +0200
     1.2 +++ b/src/Pure/ML-Systems/smlnj-0.93.ML	Mon Aug 02 15:39:23 1999 +0200
     1.3 @@ -9,6 +9,15 @@
     1.4  (*needs the Basis Library emulation*)
     1.5  use "basis.ML";
     1.6  
     1.7 +structure String =
     1.8 +struct
     1.9 +  fun substring args = String.substring args
    1.10 +    handle String.Substring => raise Subscript;
    1.11 +  fun isPrefix s1 s2 = (s1 = substring(s2,0, size s1))
    1.12 +    handle Subscript => false;
    1.13 +end;
    1.14 +
    1.15 +
    1.16  
    1.17  (** ML system related **)
    1.18