# HG changeset patch
# User wenzelm
# Date 1219847538 -7200
# Node ID 2cc19d1d4a427c9da3e3bff8caf58451b78ada99
# Parent  32acf3c6cd1202bfd9c7439d7127ba9e547aea59
added find_substring;

diff -r 32acf3c6cd12 -r 2cc19d1d4a42 src/Pure/library.ML
--- 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);