src/Pure/library.ML
changeset 29882 29154e67731d
parent 29209 c2a750c8a37b
child 30190 479806475f3c
     1.1 --- a/src/Pure/library.ML	Thu Feb 12 12:35:45 2009 -0800
     1.2 +++ b/src/Pure/library.ML	Fri Feb 13 07:53:38 2009 +1100
     1.3 @@ -159,6 +159,7 @@
     1.4    val replicate_string: int -> string -> string
     1.5    val translate_string: (string -> string) -> string -> string
     1.6    val multiply: 'a list -> 'a list list -> 'a list list
     1.7 +  val match_string: string -> string -> bool
     1.8  
     1.9    (*lists as sets -- see also Pure/General/ord_list.ML*)
    1.10    val member: ('b * 'a -> bool) -> 'a list -> 'b -> bool
    1.11 @@ -554,7 +555,6 @@
    1.12  fun multiply [] _ = []
    1.13    | multiply (x :: xs) yss = map (cons x) yss @ multiply xs yss;
    1.14  
    1.15 -
    1.16  (* direct product *)
    1.17  
    1.18  fun map_product f _ [] = []
    1.19 @@ -787,7 +787,16 @@
    1.20        if k mod 2 = 0 then replicate_string (k div 2) (a ^ a)
    1.21        else replicate_string (k div 2) (a ^ a) ^ a;
    1.22  
    1.23 -
    1.24 +(*crude matching of str against simple glob pat*)
    1.25 +fun match_string pat str =
    1.26 +  let
    1.27 +    fun match [] _ = true
    1.28 +      | match (p :: ps) s =
    1.29 +          size p <= size s andalso
    1.30 +            (case try (unprefix p) s of
    1.31 +              SOME s' => match ps s'
    1.32 +            | NONE => match (p :: ps) (String.substring (s, 1, size s - 1)));
    1.33 +  in match (space_explode "*" pat) str end;
    1.34  
    1.35  (** lists as sets -- see also Pure/General/ord_list.ML **)
    1.36