104 session.document(c.id).getOrElse(doc_or_pred(c.parent.get)) |
104 session.document(c.id).getOrElse(doc_or_pred(c.parent.get)) |
105 |
105 |
106 def current_document() = doc_or_pred(current_change) |
106 def current_document() = doc_or_pred(current_change) |
107 |
107 |
108 |
108 |
109 /* update to desired version */ |
|
110 |
|
111 def set_version(goal: Change) |
|
112 { |
|
113 // changes in buffer must be ignored |
|
114 buffer.removeBufferListener(buffer_listener) |
|
115 |
|
116 def apply(change: Change): Unit = |
|
117 change.edits.foreach { |
|
118 case Insert(start, text) => buffer.insert(start, text) |
|
119 case Remove(start, text) => buffer.remove(start, text.length) |
|
120 } |
|
121 |
|
122 def unapply(change: Change): Unit = |
|
123 change.edits.reverse.foreach { |
|
124 case Insert(start, text) => buffer.remove(start, text.length) |
|
125 case Remove(start, text) => buffer.insert(start, text) |
|
126 } |
|
127 |
|
128 // undo/redo changes |
|
129 val ancs_current = current_change.ancestors |
|
130 val ancs_goal = goal.ancestors |
|
131 val paired = ancs_current.reverse zip ancs_goal.reverse |
|
132 def last_common[A](xs: List[(A, A)]): Option[A] = { |
|
133 xs match { |
|
134 case (x, y) :: xs => |
|
135 if (x == y) |
|
136 xs match { |
|
137 case (a, b) :: ys => |
|
138 if (a == b) last_common(xs) |
|
139 else Some(x) |
|
140 case _ => Some(x) |
|
141 } |
|
142 else None |
|
143 case _ => None |
|
144 } |
|
145 } |
|
146 val common_anc = last_common(paired).get |
|
147 |
|
148 ancs_current.takeWhile(_ != common_anc) map unapply |
|
149 ancs_goal.takeWhile(_ != common_anc).reverse map apply |
|
150 |
|
151 current_change = goal |
|
152 // invoke repaint |
|
153 buffer.propertiesChanged() |
|
154 // invalidate_all() FIXME |
|
155 // overview.repaint() FIXME |
|
156 |
|
157 // track changes in buffer |
|
158 buffer.addBufferListener(buffer_listener) |
|
159 } |
|
160 |
|
161 |
|
162 /* transforming offsets */ |
109 /* transforming offsets */ |
163 |
110 |
164 private def changes_from(doc: Proof_Document): List[Edit] = |
111 private def changes_from(doc: Proof_Document): List[Edit] = |
165 List.flatten(current_change.ancestors(_.id == doc.id).reverse.map(_.edits)) ::: |
112 List.flatten(current_change.ancestors(_.id == doc.id).reverse.map(_.edits)) ::: |
166 edits.toList |
113 edits.toList |