--- a/src/Pure/library.ML Wed Aug 27 12:01:59 2008 +0200
+++ b/src/Pure/library.ML Wed Aug 27 16:32:18 2008 +0200
@@ -142,6 +142,7 @@
val fold_string: (string -> 'a -> 'a) -> string -> 'a -> 'a
val exists_string: (string -> bool) -> string -> bool
val forall_string: (string -> bool) -> string -> bool
+ val find_substring: string -> string -> int option
val enclose: string -> string -> string -> string
val unenclose: string -> string
val quote: string -> string
@@ -731,6 +732,16 @@
fun forall_string pred = not o exists_string (not o pred);
+fun find_substring s str =
+ let
+ val n = size s;
+ val len = size str;
+ fun find i =
+ if i + n > len then NONE
+ else if String.substring (str, i, n) = s then SOME i
+ else find (i + 1);
+ in find 0 end;
+
(*enclose in brackets*)
fun enclose lpar rpar str = lpar ^ str ^ rpar;
fun unenclose str = String.substring (str, 1, size str - 2);