tuned;
authorwenzelm
Fri, 10 Aug 2012 13:15:00 +0200
changeset 48753 5e57a6f24cdb
parent 48752 8a81ef0bc790
child 48754 c2c1e5944536
tuned;
src/Pure/General/linear_set.scala
--- a/src/Pure/General/linear_set.scala	Fri Aug 10 10:23:54 2012 +0200
+++ b/src/Pure/General/linear_set.scala	Fri Aug 10 13:15:00 2012 +0200
@@ -34,8 +34,6 @@
 {
   override def companion: GenericCompanion[Linear_Set] = Linear_Set
 
-  def reverse: Linear_Set[A] = new Linear_Set(end, start, prevs, nexts)
-
 
   /* relative addressing */
 
@@ -76,7 +74,7 @@
             }
       }
 
-  def append_after(hook: Option[A], elems: Seq[A]): Linear_Set[A] =
+  def append_after(hook: Option[A], elems: Seq[A]): Linear_Set[A] =  // FIXME reverse fold
     ((hook, this) /: elems) {
       case ((last, set), elem) => (Some(elem), set.insert_after(last, elem))
     }._2
@@ -147,6 +145,10 @@
         case Some(stop) => iterator(from).takeWhile(_ != stop)
       }
 
+  def reverse: Linear_Set[A] = new Linear_Set(end, start, prevs, nexts)
+
+  override def last: A = reverse.head
+
   def + (elem: A): Linear_Set[A] = insert_after(end, elem)
 
   def - (elem: A): Linear_Set[A] =