equal
deleted
inserted
replaced
42 { |
42 { |
43 def map[B](f: A => B): Edit[B] = |
43 def map[B](f: A => B): Edit[B] = |
44 this match { |
44 this match { |
45 case Remove() => Remove() |
45 case Remove() => Remove() |
46 case Edits(es) => Edits(es.map(f)) |
46 case Edits(es) => Edits(es.map(f)) |
|
47 case Update_Header(header: Header) => Update_Header(header) |
47 } |
48 } |
48 } |
49 } |
49 case class Remove[A]() extends Edit[A] |
50 case class Remove[A]() extends Edit[A] |
50 case class Edits[A](edits: List[A]) extends Edit[A] |
51 case class Edits[A](edits: List[A]) extends Edit[A] |
|
52 case class Update_Header[A](header: Header) extends Edit[A] |
51 |
53 |
52 sealed case class Header(val master_dir: Path, val thy_header: Exn.Result[Thy_Header.Header]) |
54 sealed case class Header(val master_dir: Path, val thy_header: Exn.Result[Thy_Header.Header]) |
53 val empty_header = Header(Path.current, Exn.Exn(ERROR("Bad theory header"))) |
55 val empty_header = Header(Path.current, Exn.Exn(ERROR("Bad theory header"))) |
54 |
56 |
55 val empty: Node = Node(empty_header, Map(), Linear_Set()) |
57 val empty: Node = Node(empty_header, Map(), Linear_Set()) |