# HG changeset patch
# User wenzelm
# Date 902761027 -7200
# Node ID 2d1425492fb3a579986fb9c6c9e58583cfc48644
# Parent  c77e9dd9bafca89f4bbb65dcebc1f61003d96c6f
val single: 'a -> 'a list;
val suffix: string -> string -> string;
val unsuffix: string -> string -> string;

diff -r c77e9dd9bafc -r 2d1425492fb3 src/Pure/library.ML
--- a/src/Pure/library.ML	Mon Aug 10 11:51:09 1998 +0200
+++ b/src/Pure/library.ML	Mon Aug 10 16:57:07 1998 +0200
@@ -69,6 +69,7 @@
   val hd: 'a list -> 'a
   val tl: 'a list -> 'a list
   val cons: 'a -> 'a list -> 'a list
+  val single: 'a -> 'a list
   val append: 'a list -> 'a list -> 'a list
   val foldl: ('a * 'b -> 'a) -> 'a * 'b list -> 'a
   val foldr: ('a * 'b -> 'b) -> 'a list * 'b -> 'b
@@ -124,6 +125,8 @@
   val cat_lines: string list -> string
   val space_explode: string -> string -> string list
   val split_lines: string -> string list
+  val suffix: string -> string -> string
+  val unsuffix: string -> string -> string
 
   (*lists as sets*)
   val mem: ''a * ''a list -> bool
@@ -383,6 +386,7 @@
   | tl (_ :: xs) = xs;
 
 fun cons x xs = x :: xs;
+fun single x = [x];
 
 fun append xs ys = xs @ ys;
 
@@ -662,6 +666,20 @@
 
 val split_lines = space_explode "\n";
 
+(*append suffix*)
+fun suffix sfx s = s ^ sfx;
+
+(*remove suffix*)
+fun unsuffix sfx s =
+  let
+    val cs = explode s;
+    val prfx_len = size s - size sfx;
+  in
+    if prfx_len >= 0 andalso implode (drop (prfx_len, cs)) = sfx then
+      implode (take (prfx_len, cs))
+    else raise LIST "unsuffix"
+  end;
+
 
 
 (** lists as sets **)