corrected order
authorimmler@in.tum.de
Mon, 07 Sep 2009 13:52:36 +0200
changeset 3472139e3039645ae
parent 34720 3f32e08bbb6c
child 34722 f5b408849dcc
corrected order
src/Tools/jEdit/src/jedit/TheoryView.scala
     1.1 --- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Sun Sep 06 22:27:32 2009 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Mon Sep 07 13:52:36 2009 +0200
     1.3 @@ -197,14 +197,15 @@
     1.4  
     1.5    /* transforming offsets */
     1.6  
     1.7 -  private def changes_to(doc: ProofDocument): List[Edit] =
     1.8 -    edits.toList ::: List.flatten(current_change.ancestors(_.id == doc.id).map(_.edits))
     1.9 +  private def changes_from(doc: ProofDocument): List[Edit] =
    1.10 +    List.flatten(current_change.ancestors(_.id == doc.id).reverse.map(_.edits)) :::
    1.11 +      edits.toList
    1.12  
    1.13    def from_current(doc: ProofDocument, offset: Int): Int =
    1.14 -    (offset /: changes_to(doc)) ((i, change) => change before i)
    1.15 +    (offset /: changes_from(doc).reverse) ((i, change) => change before i)
    1.16  
    1.17    def to_current(doc: ProofDocument, offset: Int): Int =
    1.18 -    (offset /: changes_to(doc).reverse) ((i, change) => change after i)
    1.19 +    (offset /: changes_from(doc)) ((i, change) => change after i)
    1.20  
    1.21  
    1.22    private def lines_of_command(cmd: Command) =