equal
deleted
inserted
replaced
195 override def transactionComplete(buffer: JEditBuffer) { } |
195 override def transactionComplete(buffer: JEditBuffer) { } |
196 |
196 |
197 |
197 |
198 /* transforming offsets */ |
198 /* transforming offsets */ |
199 |
199 |
200 private def changes_to(doc: ProofDocument): List[Edit] = |
200 private def changes_from(doc: ProofDocument): List[Edit] = |
201 edits.toList ::: List.flatten(current_change.ancestors(_.id == doc.id).map(_.edits)) |
201 List.flatten(current_change.ancestors(_.id == doc.id).reverse.map(_.edits)) ::: |
|
202 edits.toList |
202 |
203 |
203 def from_current(doc: ProofDocument, offset: Int): Int = |
204 def from_current(doc: ProofDocument, offset: Int): Int = |
204 (offset /: changes_to(doc)) ((i, change) => change before i) |
205 (offset /: changes_from(doc).reverse) ((i, change) => change before i) |
205 |
206 |
206 def to_current(doc: ProofDocument, offset: Int): Int = |
207 def to_current(doc: ProofDocument, offset: Int): Int = |
207 (offset /: changes_to(doc).reverse) ((i, change) => change after i) |
208 (offset /: changes_from(doc)) ((i, change) => change after i) |
208 |
209 |
209 |
210 |
210 private def lines_of_command(cmd: Command) = |
211 private def lines_of_command(cmd: Command) = |
211 { |
212 { |
212 val document = current_document() |
213 val document = current_document() |