equal
deleted
inserted
replaced
42 { |
42 { |
43 sealed abstract class Edit[A] |
43 sealed abstract class Edit[A] |
44 { |
44 { |
45 def map[B](f: A => B): Edit[B] = |
45 def map[B](f: A => B): Edit[B] = |
46 this match { |
46 this match { |
47 case Remove() => Remove() |
47 case Clear() => Clear() |
48 case Edits(es) => Edits(es.map(f)) |
48 case Edits(es) => Edits(es.map(f)) |
49 case Header(header) => Header(header) |
49 case Header(header) => Header(header) |
50 } |
50 } |
51 } |
51 } |
52 case class Remove[A]() extends Edit[A] |
52 case class Clear[A]() extends Edit[A] |
53 case class Edits[A](edits: List[A]) extends Edit[A] |
53 case class Edits[A](edits: List[A]) extends Edit[A] |
54 case class Header[A](header: Node_Header) extends Edit[A] |
54 case class Header[A](header: Node_Header) extends Edit[A] |
55 |
55 |
56 def norm_header[A](f: String => String, header: Node_Header): Header[A] = |
56 def norm_header[A](f: String => String, header: Node_Header): Header[A] = |
57 header match { |
57 header match { |