src/Tools/jEdit/src/jedit/TheoryView.scala
changeset 34718 39e3039645ae
parent 34717 3f32e08bbb6c
child 34719 f5b408849dcc
equal deleted inserted replaced
34717:3f32e08bbb6c 34718:39e3039645ae
   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()