# HG changeset patch
# User wenzelm
# Date 1515958767 -3600
# Node ID a38c74b0886d54a5402d26887e81784425b60935
# Parent  e0c0c1f0e3e797e8d072f0b31533239dedf84376
more operations (as in ML);

diff -r e0c0c1f0e3e7 -r a38c74b0886d src/Pure/library.scala
--- a/src/Pure/library.scala	Sun Jan 14 20:10:11 2018 +0100
+++ b/src/Pure/library.scala	Sun Jan 14 20:39:27 2018 +0100
@@ -223,6 +223,15 @@
   def take_prefix[A](pred: A => Boolean, xs: List[A]): (List[A], List[A]) =
     (xs.takeWhile(pred), xs.dropWhile(pred))
 
+  def take_suffix[A](pred: A => Boolean, xs: List[A]): (List[A], List[A]) =
+  {
+    val rev_xs = xs.reverse
+    (rev_xs.dropWhile(pred).reverse, rev_xs.takeWhile(pred).reverse)
+  }
+
+  def trim[A](pred: A => Boolean, xs: List[A]): List[A] =
+    take_suffix(pred, take_prefix(pred, xs)._2)._1
+
   def member[A, B](xs: List[A])(x: B): Boolean = xs.contains(x)
   def insert[A](x: A)(xs: List[A]): List[A] = if (xs.contains(x)) xs else x :: xs
   def remove[A, B](x: B)(xs: List[A]): List[A] = if (member(xs)(x)) xs.filterNot(_ == x) else xs