1.1 --- a/src/Pure/PIDE/change.scala	Thu Aug 05 18:00:37 2010 +0200
     1.2 +++ b/src/Pure/PIDE/change.scala	Thu Aug 05 18:13:12 2010 +0200
     1.3 @@ -17,8 +17,8 @@
     1.4      val document: Document
     1.5      val node: Document.Node
     1.6      val is_outdated: Boolean
     1.7 -    def from_current(offset: Int): Int
     1.8 -    def to_current(offset: Int): Int
     1.9 +    def convert(offset: Int): Int
    1.10 +    def revert(offset: Int): Int
    1.11    }
    1.12  }
    1.13  
    1.14 @@ -74,10 +74,8 @@
    1.15        val document = stable.join_document
    1.16        val node = document.nodes(name)
    1.17        val is_outdated = !(extra_edits.isEmpty && latest == stable)
    1.18 -      def from_current(offset: Int): Int =
    1.19 -        (offset /: changes.reverse)((i, change) => change before i)  // FIXME fold_rev (!?)
    1.20 -      def to_current(offset: Int): Int =
    1.21 -        (offset /: changes)((i, change) => change after i)
    1.22 +      def convert(offset: Int): Int = (offset /: changes)((i, change) => change after i)
    1.23 +      def revert(offset: Int): Int = (offset /: changes.reverse)((i, change) => change before i)  // FIXME fold_rev (!?)
    1.24      }
    1.25    }
    1.26  }
    1.27 \ No newline at end of file

     2.1 --- a/src/Tools/jEdit/src/jedit/document_view.scala	Thu Aug 05 18:00:37 2010 +0200
     2.2 +++ b/src/Tools/jEdit/src/jedit/document_view.scala	Thu Aug 05 18:13:12 2010 +0200
     2.3 @@ -126,8 +126,8 @@
     2.4      for ((command, start) <- snapshot.node.command_starts) {
     2.5        if (changed(command)) {
     2.6          val stop = start + command.length
     2.7 -        val line1 = buffer.getLineOfOffset(snapshot.to_current(start))
     2.8 -        val line2 = buffer.getLineOfOffset(snapshot.to_current(stop))
     2.9 +        val line1 = buffer.getLineOfOffset(snapshot.convert(start))
    2.10 +        val line2 = buffer.getLineOfOffset(snapshot.convert(stop))
    2.11          if (line2 >= text_area.getFirstLine &&
    2.12              line1 <= text_area.getFirstLine + text_area.getVisibleLines)
    2.13            visible_change = true
    2.14 @@ -153,7 +153,7 @@
    2.15  
    2.16          val command_range: Iterable[(Command, Int)] =
    2.17          {
    2.18 -          val range = snapshot.node.command_range(snapshot.from_current(start(0)))
    2.19 +          val range = snapshot.node.command_range(snapshot.revert(start(0)))
    2.20            if (range.hasNext) {
    2.21              val (cmd0, start0) = range.next
    2.22              new Iterable[(Command, Int)] {
    2.23 @@ -171,17 +171,17 @@
    2.24                val line_start = start(i)
    2.25                val line_end = model.visible_line_end(line_start, end(i))
    2.26  
    2.27 -              val a = snapshot.from_current(line_start)
    2.28 -              val b = snapshot.from_current(line_end)
    2.29 +              val a = snapshot.revert(line_start)
    2.30 +              val b = snapshot.revert(line_end)
    2.31                val cmds = command_range.iterator.
    2.32                  dropWhile { case (cmd, c) => c + cmd.length <= a } .
    2.33                  takeWhile { case (_, c) => c < b }
    2.34  
    2.35                for ((command, command_start) <- cmds if !command.is_ignored) {
    2.36 -                val p = text_area.offsetToXY(
    2.37 -                  line_start max snapshot.to_current(command_start))
    2.38 -                val q = text_area.offsetToXY(
    2.39 -                  line_end min snapshot.to_current(command_start + command.length))
    2.40 +                val p =
    2.41 +                  text_area.offsetToXY(line_start max snapshot.convert(command_start))
    2.42 +                val q =
    2.43 +                  text_area.offsetToXY(line_end min snapshot.convert(command_start + command.length))
    2.44                  assert(p.y == q.y)
    2.45                  gfx.setColor(Document_View.choose_color(snapshot, command))
    2.46                  gfx.fillRect(p.x, y, q.x - p.x, line_height)
    2.47 @@ -197,7 +197,7 @@
    2.48      override def getToolTipText(x: Int, y: Int): String =
    2.49      {
    2.50        val snapshot = model.snapshot()
    2.51 -      val offset = snapshot.from_current(text_area.xyToOffset(x, y))
    2.52 +      val offset = snapshot.revert(text_area.xyToOffset(x, y))
    2.53        snapshot.node.command_at(offset) match {
    2.54          case Some((command, command_start)) =>
    2.55            snapshot.document.current_state(command).type_at(offset - command_start) match {
    2.56 @@ -267,8 +267,8 @@
    2.57        val saved_color = gfx.getColor  // FIXME needed!?
    2.58        try {
    2.59          for ((command, start) <- snapshot.node.command_starts if !command.is_ignored) {
    2.60 -          val line1 = buffer.getLineOfOffset(snapshot.to_current(start))
    2.61 -          val line2 = buffer.getLineOfOffset(snapshot.to_current(start + command.length)) + 1
    2.62 +          val line1 = buffer.getLineOfOffset(snapshot.convert(start))
    2.63 +          val line2 = buffer.getLineOfOffset(snapshot.convert(start + command.length)) + 1
    2.64            val y = line_to_y(line1)
    2.65            val height = HEIGHT * (line2 - line1)
    2.66            gfx.setColor(Document_View.choose_color(snapshot, command))

     3.1 --- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Thu Aug 05 18:00:37 2010 +0200
     3.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Thu Aug 05 18:13:12 2010 +0200
     3.3 @@ -43,14 +43,14 @@
     3.4      Document_Model(buffer) match {
     3.5        case Some(model) =>
     3.6          val snapshot = model.snapshot()
     3.7 -        val offset = snapshot.from_current(original_offset)
     3.8 +        val offset = snapshot.revert(original_offset)
     3.9          snapshot.node.command_at(offset) match {
    3.10            case Some((command, command_start)) =>
    3.11              snapshot.document.current_state(command).ref_at(offset - command_start) match {
    3.12                case Some(ref) =>
    3.13 -                val begin = snapshot.to_current(command_start + ref.start)
    3.14 +                val begin = snapshot.convert(command_start + ref.start)
    3.15                  val line = buffer.getLineOfOffset(begin)
    3.16 -                val end = snapshot.to_current(command_start + ref.stop)
    3.17 +                val end = snapshot.convert(command_start + ref.stop)
    3.18                  ref.info match {
    3.19                    case Command.RefInfo(Some(ref_file), Some(ref_line), _, _) =>
    3.20                      new External_Hyperlink(begin, end, line, ref_file, ref_line)
    3.21 @@ -60,7 +60,7 @@
    3.22                          snapshot.node.command_start(ref_cmd) match {
    3.23                            case Some(ref_cmd_start) =>
    3.24                              new Internal_Hyperlink(begin, end, line,
    3.25 -                              snapshot.to_current(ref_cmd_start + offset - 1))
    3.26 +                              snapshot.convert(ref_cmd_start + offset - 1))
    3.27                            case None => null // FIXME external ref
    3.28                          }
    3.29                        case _ => null

     4.1 --- a/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala	Thu Aug 05 18:00:37 2010 +0200
     4.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala	Thu Aug 05 18:13:12 2010 +0200
     4.3 @@ -165,10 +165,10 @@
     4.4      var next_x = start
     4.5      for {
     4.6        (command, command_start) <-
     4.7 -        snapshot.node.command_range(snapshot.from_current(start), snapshot.from_current(stop))
     4.8 +        snapshot.node.command_range(snapshot.revert(start), snapshot.revert(stop))
     4.9        markup <- snapshot.document.current_state(command).highlight.flatten
    4.10 -      val abs_start = snapshot.to_current(command_start + markup.start)
    4.11 -      val abs_stop = snapshot.to_current(command_start + markup.stop)
    4.12 +      val abs_start = snapshot.convert(command_start + markup.start)
    4.13 +      val abs_stop = snapshot.convert(command_start + markup.stop)
    4.14        if (abs_stop > start)
    4.15        if (abs_start < stop)
    4.16        val token_start = (abs_start - start) max 0