src/Pure/library.ML
changeset 5285 2d1425492fb3
parent 5112 9e74cf11e4a4
child 5893 c755dfd02509
     1.1 --- a/src/Pure/library.ML	Mon Aug 10 11:51:09 1998 +0200
     1.2 +++ b/src/Pure/library.ML	Mon Aug 10 16:57:07 1998 +0200
     1.3 @@ -69,6 +69,7 @@
     1.4    val hd: 'a list -> 'a
     1.5    val tl: 'a list -> 'a list
     1.6    val cons: 'a -> 'a list -> 'a list
     1.7 +  val single: 'a -> 'a list
     1.8    val append: 'a list -> 'a list -> 'a list
     1.9    val foldl: ('a * 'b -> 'a) -> 'a * 'b list -> 'a
    1.10    val foldr: ('a * 'b -> 'b) -> 'a list * 'b -> 'b
    1.11 @@ -124,6 +125,8 @@
    1.12    val cat_lines: string list -> string
    1.13    val space_explode: string -> string -> string list
    1.14    val split_lines: string -> string list
    1.15 +  val suffix: string -> string -> string
    1.16 +  val unsuffix: string -> string -> string
    1.17  
    1.18    (*lists as sets*)
    1.19    val mem: ''a * ''a list -> bool
    1.20 @@ -383,6 +386,7 @@
    1.21    | tl (_ :: xs) = xs;
    1.22  
    1.23  fun cons x xs = x :: xs;
    1.24 +fun single x = [x];
    1.25  
    1.26  fun append xs ys = xs @ ys;
    1.27  
    1.28 @@ -662,6 +666,20 @@
    1.29  
    1.30  val split_lines = space_explode "\n";
    1.31  
    1.32 +(*append suffix*)
    1.33 +fun suffix sfx s = s ^ sfx;
    1.34 +
    1.35 +(*remove suffix*)
    1.36 +fun unsuffix sfx s =
    1.37 +  let
    1.38 +    val cs = explode s;
    1.39 +    val prfx_len = size s - size sfx;
    1.40 +  in
    1.41 +    if prfx_len >= 0 andalso implode (drop (prfx_len, cs)) = sfx then
    1.42 +      implode (take (prfx_len, cs))
    1.43 +    else raise LIST "unsuffix"
    1.44 +  end;
    1.45 +
    1.46  
    1.47  
    1.48  (** lists as sets **)