# HG changeset patch # User wenzelm # Date 1742934279 -3600 # Node ID f3fbe96bd7185eafdbf30205654f1f6249192344 # Parent 47c4ea946fc8cb1fe68b9fa5ae6b36bec0c598c0 tuned (see also 20b261654e33); diff -r 47c4ea946fc8 -r f3fbe96bd718 src/Pure/General/linear_set.scala --- a/src/Pure/General/linear_set.scala Tue Mar 25 15:53:54 2025 +0100 +++ b/src/Pure/General/linear_set.scala Tue Mar 25 21:24:39 2025 +0100 @@ -37,10 +37,12 @@ final class Linear_Set[A] private( start: Option[A], end: Option[A], - val nexts: Map[A, A], prevs: Map[A, A]) - extends Iterable[A] + nexts: Map[A, A], + prevs: Map[A, A] +) extends Iterable[A] with SetOps[A, Linear_Set, Linear_Set[A]] with IterableFactoryDefaults[A, Linear_Set] { + /* relative addressing */ def next(elem: A): Option[A] =