equal
deleted
inserted
replaced
51 } |
51 } |
52 case class Remove[A]() extends Edit[A] |
52 case class Remove[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: Path => 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 { |
58 case Exn.Res(h) => Header[A](Exn.capture { h.norm_deps(name => f(Path.explode(name))) }) |
58 case Exn.Res(h) => Header[A](Exn.capture { h.norm_deps(f) }) |
59 case exn => Header[A](exn) |
59 case exn => Header[A](exn) |
60 } |
60 } |
61 |
61 |
62 val empty: Node = Node(Exn.Exn(ERROR("Bad theory header")), Map(), Linear_Set()) |
62 val empty: Node = Node(Exn.Exn(ERROR("Bad theory header")), Map(), Linear_Set()) |
63 |
63 |