32 /* named nodes -- development graph */ |
32 /* named nodes -- development graph */ |
33 |
33 |
34 type Edit[A] = (String, Node.Edit[A]) |
34 type Edit[A] = (String, Node.Edit[A]) |
35 type Edit_Text = Edit[Text.Edit] |
35 type Edit_Text = Edit[Text.Edit] |
36 type Edit_Command = Edit[(Option[Command], Option[Command])] |
36 type Edit_Command = Edit[(Option[Command], Option[Command])] |
37 type Edit_Command_ID = Edit[(Option[Command_ID], Option[Command_ID])] |
|
38 |
37 |
39 type Node_Header = Exn.Result[Thy_Header] |
38 type Node_Header = Exn.Result[Thy_Header] |
40 |
39 |
41 object Node |
40 object Node |
42 { |
41 { |
43 sealed abstract class Edit[A] |
42 sealed abstract class Edit[A] |
44 { |
43 { |
45 def map[B](f: A => B): Edit[B] = |
44 def foreach(f: A => Unit) |
|
45 { |
46 this match { |
46 this match { |
47 case Clear() => Clear() |
47 case Edits(es) => es.foreach(f) |
48 case Edits(es) => Edits(es.map(f)) |
48 case _ => |
49 case Header(header) => Header(header) |
|
50 } |
49 } |
|
50 } |
51 } |
51 } |
52 case class Clear[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 |