src/Pure/General/linear_set.scala
changeset 42718 d7b2625c1193
parent 38583 ff7f9510b0d6
child 46620 9aea30f3b954
equal deleted inserted replaced
42717:0bbb56867091 42718:d7b2625c1193
    12   GenericSetTemplate, GenericCompanion}
    12   GenericSetTemplate, GenericCompanion}
    13 
    13 
    14 
    14 
    15 object Linear_Set extends ImmutableSetFactory[Linear_Set]
    15 object Linear_Set extends ImmutableSetFactory[Linear_Set]
    16 {
    16 {
    17   private case class Rep[A](
    17   protected case class Rep[A](
    18     val start: Option[A], val end: Option[A], val nexts: Map[A, A], prevs: Map[A, A])
    18     val start: Option[A], val end: Option[A], val nexts: Map[A, A], prevs: Map[A, A])
    19 
    19 
    20   private def empty_rep[A] = Rep[A](None, None, Map(), Map())
    20   private def empty_rep[A] = Rep[A](None, None, Map(), Map())
    21 
    21 
    22   private def make[A](start: Option[A], end: Option[A], nexts: Map[A, A], prevs: Map[A, A])
    22   private def make[A](start: Option[A], end: Option[A], nexts: Map[A, A], prevs: Map[A, A])