src/Pure/library.scala
changeset 63781 af9fe0b6b78e
parent 63773 d1a5d10affc0
child 63789 af28929ff219
--- a/src/Pure/library.scala	Sun Sep 04 20:31:23 2016 +0200
+++ b/src/Pure/library.scala	Sun Sep 04 21:09:18 2016 +0200
@@ -8,6 +8,7 @@
 package isabelle
 
 
+import scala.annotation.tailrec
 import scala.collection.mutable
 import scala.util.matching.Regex
 
@@ -194,4 +195,18 @@
     xs.foreach(x => if (!result.contains(x)) result += x)
     result.toList
   }
+
+  def duplicates[A](lst: List[A]): List[A] =
+  {
+    val result = new mutable.ListBuffer[A]
+    @tailrec def dups(rest: List[A]): Unit =
+      rest match {
+        case Nil =>
+        case x :: xs =>
+          if (!result.contains(x) && xs.contains(x)) result += x
+          dups(xs)
+      }
+    dups(lst)
+    result.toList
+  }
 }