64 } |
64 } |
65 } |
65 } |
66 case class Clear[A, B]() extends Edit[A, B] |
66 case class Clear[A, B]() extends Edit[A, B] |
67 case class Edits[A, B](edits: List[A]) extends Edit[A, B] |
67 case class Edits[A, B](edits: List[A]) extends Edit[A, B] |
68 case class Deps[A, B](header: Header) extends Edit[A, B] |
68 case class Deps[A, B](header: Header) extends Edit[A, B] |
69 case class Perspective[A, B](perspective: B) extends Edit[A, B] |
69 case class Perspective[A, B](required: Boolean, perspective: B) extends Edit[A, B] |
|
70 type Perspective_Text = Perspective[Text.Edit, Text.Perspective] |
70 |
71 |
71 def command_starts(commands: Iterator[Command], offset: Text.Offset = 0) |
72 def command_starts(commands: Iterator[Command], offset: Text.Offset = 0) |
72 : Iterator[(Command, Text.Offset)] = |
73 : Iterator[(Command, Text.Offset)] = |
73 { |
74 { |
74 var i = offset |
75 var i = offset |
84 val empty: Node = new Node() |
85 val empty: Node = new Node() |
85 } |
86 } |
86 |
87 |
87 final class Node private( |
88 final class Node private( |
88 val header: Node.Header = Node.bad_header("Bad theory header"), |
89 val header: Node.Header = Node.bad_header("Bad theory header"), |
89 val perspective: Command.Perspective = Command.Perspective.empty, |
90 val perspective: (Boolean, Command.Perspective) = (false, Command.Perspective.empty), |
90 val commands: Linear_Set[Command] = Linear_Set.empty) |
91 val commands: Linear_Set[Command] = Linear_Set.empty) |
91 { |
92 { |
92 def clear: Node = new Node(header = header) |
93 def clear: Node = new Node(header = header) |
93 |
94 |
94 def update_header(new_header: Node.Header): Node = |
95 def update_header(new_header: Node.Header): Node = |
95 new Node(new_header, perspective, commands) |
96 new Node(new_header, perspective, commands) |
96 |
97 |
97 def update_perspective(new_perspective: Command.Perspective): Node = |
98 def update_perspective(new_perspective: (Boolean, Command.Perspective)): Node = |
98 new Node(header, new_perspective, commands) |
99 new Node(header, new_perspective, commands) |
|
100 |
|
101 def same_perspective(other: (Boolean, Command.Perspective)): Boolean = |
|
102 perspective._1 == other._1 && (perspective._2 same other._2) |
99 |
103 |
100 def update_commands(new_commands: Linear_Set[Command]): Node = |
104 def update_commands(new_commands: Linear_Set[Command]): Node = |
101 new Node(header, perspective, new_commands) |
105 new Node(header, perspective, new_commands) |
102 |
106 |
103 |
107 |